(* subset less or equal (inclusion) *)
definition sle: \forall D. Subset D \to Subset D \to Prop \def
- \lambda D,U1,U2. \forall d. U1 d \to U2 d.
-(*
+ \lambda D,U1,U2. \iforall d. U1 d \to U2 d.
+
(* subset overlap *)
definition sover: \forall D. Subset D \to Subset D \to Prop \def
- \lambda D,U1,U2. \forall d. U1 d \to U2 d.
-*)
+ \lambda D,U1,U2. \iexists d. U1 d \land U2 d.
(* coercions **************************************************************)
\lambda (D:Domain). \lambda U.
mk_Domain (mk_Class D (sin D U) (cle1 D)).
-coercion domain_of_subset.
+coercion cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs/domain_of_subset.con.
(* the full subset of a domain *)
coercion stop.
-