X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fsets.ma;h=8e40b666bfdee2eb318478d2899a3bece809619f;hb=bf816f05ddbe0ded4948dd33490619724dc4f7cf;hp=4d77f6c2f86f5808bbdbe6e416ca6676969e6f86;hpb=2327897158cc01b63c68d3b82872c17159fbb8e6;p=helm.git

diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma
index 4d77f6c2f..8e40b666b 100644
--- a/matita/matita/lib/basics/sets.ma
+++ b/matita/matita/lib/basics/sets.ma
@@ -10,6 +10,8 @@
       V_______________________________________________________________ *)
 
 include "basics/logic.ma".
+include "basics/core_notation/singl_1.ma".
+include "basics/core_notation/subseteq_2.ma".
 
 (**** a subset of A is just an object of type A→Prop ****)
 
@@ -38,81 +40,82 @@ interpretation "subset" 'subseteq a b = (subset ? a b).
 
 (* extensional equality *)
 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
-notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
+(* ≐ is typed as \doteq *)
+notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
 
 lemma eqP_sym: ∀U.∀A,B:U →Prop. 
-  A =1 B → B =1 A.
+  A ≐ B → B ≐ A.
 #U #A #B #eqAB #a @iff_sym @eqAB qed.
  
 lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
-  A =1 B → B =1 C → A =1 C.
+  A ≐ B → B ≐ C → A ≐ C.
 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
 
 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
-  A =1 C  → A ∪ B =1 C ∪ B.
+  A ≐ C  → A ∪ B ≐ C ∪ B.
 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
   
 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
-  B =1 C  → A ∪ B =1 A ∪ C.
+  B ≐ C  → A ∪ B ≐ A ∪ C.
 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
   
 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. 
-  A =1 C  → A ∩ B =1 C ∩ B.
+  A ≐ C  → A ∩ B ≐ C ∩ B.
 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
   
 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
-  B =1 C  → A ∩ B =1 A ∩ C.
+  B ≐ C  → A ∩ B ≐ A ∩ C.
 #U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
 
 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
-  A =1 C  → A - B =1 C - B.
+  A ≐ C  → A - B ≐ C - B.
 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
   
 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
-  B =1 C  → A - B =1 A - C.
+  B ≐ C  → A - B ≐ A - C.
 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
 
 (* set equalities *)
 lemma union_empty_r: ∀U.∀A:U→Prop. 
-  A ∪ ∅ =1 A.
+  A ∪ ∅ ≐ A.
 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
 qed.
 
 lemma union_comm : ∀U.∀A,B:U →Prop. 
-  A ∪ B =1 B ∪ A.
+  A ∪ B ≐ B ∪ A.
 #U #A #B #a % * /2/ qed. 
 
 lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
-  A ∪ B ∪ C =1 A ∪ (B ∪ C).
+  A ∪ B ∪ C ≐ A ∪ (B ∪ C).
 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
 qed.   
 
 lemma cap_comm : ∀U.∀A,B:U →Prop. 
-  A ∩ B =1 B ∩ A.
+  A ∩ B ≐ B ∩ A.
 #U #A #B #a % * /2/ qed. 
 
 lemma union_idemp: ∀U.∀A:U →Prop. 
-  A ∪ A =1 A.
+  A ∪ A ≐ A.
 #U #A #a % [* // | /2/] qed. 
 
 lemma cap_idemp: ∀U.∀A:U →Prop. 
-  A ∩ A =1 A.
+  A ∩ A ≐ A.
 #U #A #a % [* // | /2/] qed. 
 
 (*distributivities *)
 
 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
-  (A ∪ B) ∩ C =1 (A ∩ C) ∪ (B ∩ C).
+  (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
 #U #A #B #C #w % [* * /3/ | * * /3/] 
 qed.
   
 lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
-  (A ∪ B) - C =1 (A - C) ∪ (B - C).
+  (A ∪ B) - C ≐ (A - C) ∪ (B - C).
 #U #A #B #C #w % [* * /3/ | * * /3/] 
 qed.
 
 (* substraction *)
-lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
 #U #A #B #w normalize /2/
-qed.
\ No newline at end of file
+qed.