X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Fbasics%2Fsets.ma;h=4d77f6c2f86f5808bbdbe6e416ca6676969e6f86;hb=e0827239f4b44f2af9c7f88c4c7c41f2a193ae37;hp=622025d790a65afa6269b5626b99e4d2ca329617;hpb=24fc5e5485245fe879e17d46176530b688930b3b;p=helm.git

diff --git a/matita/matita/lib/basics/sets.ma b/matita/matita/lib/basics/sets.ma
index 622025d79..4d77f6c2f 100644
--- a/matita/matita/lib/basics/sets.ma
+++ b/matita/matita/lib/basics/sets.ma
@@ -27,8 +27,14 @@ interpretation "union" 'union a b = (union ? a b).
 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
 interpretation "intersection" 'intersects a b = (intersection ? a b).
 
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+interpretation "complement" 'not a = (complement ? a).
+
+definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+interpretation "substraction" 'minus a b = (substraction ? a b).
+
 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
-interpretation "subset" 'subseteq a b = (intersection ? a b).
+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.
@@ -51,7 +57,28 @@ lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
   B =1 C  → A ∪ B =1 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.
+#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.
+#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.
+#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.
+#U #A #B #C #eqBC #a @iff_and_l /2/ qed.
+
 (* set equalities *)
+lemma union_empty_r: ∀U.∀A:U→Prop. 
+  A ∪ ∅ =1 A.
+#U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
+qed.
+
 lemma union_comm : ∀U.∀A,B:U →Prop. 
   A ∪ B =1 B ∪ A.
 #U #A #B #a % * /2/ qed. 
@@ -73,4 +100,19 @@ lemma cap_idemp: ∀U.∀A:U →Prop.
   A ∩ A =1 A.
 #U #A #a % [* // | /2/] qed. 
 
+(*distributivities *)
 
+lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
+  (A ∪ B) ∩ C =1 (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).
+#U #A #B #C #w % [* * /3/ | * * /3/] 
+qed.
+
+(* substraction *)
+lemma substract_def:∀U.∀A,B:U→Prop. A-B =1 A ∩ ¬B.
+#U #A #B #w normalize /2/
+qed.
\ No newline at end of file