]> matita.cs.unibo.it Git - helm.git/blob - weblib/basics/sets.ma
universary milestone in basic_2
[helm.git] / weblib / basics / sets.ma
1 include "basics/logic.ma".
2
3 (**** a subset of A is just an object of type A→Prop ****)
4
5 \ 5img class="anchor" src="icons/tick.png" id="empty_set"\ 6definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
6 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
7 interpretation "empty set" 'empty_set = (empty_set ?).
8
9 \ 5img class="anchor" src="icons/tick.png" id="singleton"\ 6definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6a.
10 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
11 interpretation "singleton" 'singl x = (singleton ? x).
12
13 \ 5img class="anchor" src="icons/tick.png" id="union"\ 6definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 Q a.
14 interpretation "union" 'union a b = (union ? a b).
15
16 \ 5img class="anchor" src="icons/tick.png" id="intersection"\ 6definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 Q a.
17 interpretation "intersection" 'intersects a b = (intersection ? a b).
18
19 \ 5img class="anchor" src="icons/tick.png" id="complement"\ 6definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A w.
20 interpretation "complement" 'not a = (complement ? a).
21
22 \ 5img class="anchor" src="icons/tick.png" id="substraction"\ 6definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 B w.
23 interpretation "substraction" 'minus a b = (substraction ? a b).
24
25 \ 5img class="anchor" src="icons/tick.png" id="subset"\ 6definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
26 interpretation "subset" 'subseteq a b = (subset ? a b).
27
28 (* extensional equality *)
29 \ 5img class="anchor" src="icons/tick.png" id="eqP"\ 6definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 Q a.
30 (* ≐ is typed as \doteq *)
31 notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
32 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
33
34 \ 5img class="anchor" src="icons/tick.png" id="eqP_sym"\ 6lemma eqP_sym: ∀U.∀A,B:U →Prop. 
35   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
36 #U #A #B #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @eqAB qed.
37  
38 \ 5img class="anchor" src="icons/tick.png" id="eqP_trans"\ 6lemma eqP_trans: ∀U.∀A,B,C:U →Prop. 
39   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C → A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C.
40 #U #A #B #C #eqAB #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 // qed.
41
42 \ 5img class="anchor" src="icons/tick.png" id="eqP_union_r"\ 6lemma eqP_union_r: ∀U.∀A,B,C:U →Prop. 
43   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B.
44 #U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"\ 6iff_or_r\ 5/a\ 6 @eqAB qed.
45   
46 \ 5img class="anchor" src="icons/tick.png" id="eqP_union_l"\ 6lemma eqP_union_l: ∀U.∀A,B,C:U →Prop. 
47   B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C  → A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C.
48 #U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"\ 6iff_or_l\ 5/a\ 6 @eqBC qed.
49   
50 \ 5img class="anchor" src="icons/tick.png" id="eqP_intersect_r"\ 6lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop. 
51   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B.
52 #U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
53   
54 \ 5img class="anchor" src="icons/tick.png" id="eqP_intersect_l"\ 6lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop. 
55   B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C  → A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C.
56 #U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 @eqBC qed.
57
58 \ 5img class="anchor" src="icons/tick.png" id="eqP_substract_r"\ 6lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop. 
59   A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C  → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B.
60 #U #A #B #C #eqAB #a @\ 5a href="cic:/matita/basics/logic/iff_and_r.def(2)"\ 6iff_and_r\ 5/a\ 6 @eqAB qed.
61   
62 \ 5img class="anchor" src="icons/tick.png" id="eqP_substract_l"\ 6lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop. 
63   B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C  → A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C.
64 #U #A #B #C #eqBC #a @\ 5a href="cic:/matita/basics/logic/iff_and_l.def(2)"\ 6iff_and_l\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/iff_not.def(4)"\ 6iff_not\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
65
66 (* set equalities *)
67 \ 5img class="anchor" src="icons/tick.png" id="union_empty_r"\ 6lemma union_empty_r: ∀U.∀A:U→Prop. 
68   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="empty set" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
69 #U #A #w % [* // normalize #abs @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
70 qed.
71
72 \ 5img class="anchor" src="icons/tick.png" id="union_comm"\ 6lemma union_comm : ∀U.∀A,B:U →Prop. 
73   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
74 #U #A #B #a % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
75
76 \ 5img class="anchor" src="icons/tick.png" id="union_assoc"\ 6lemma union_assoc: ∀U.∀A,B,C:U → Prop. 
77   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (B \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C).
78 #S #A #B #C #w % [* [* /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] | * [/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
79 qed.   
80
81 \ 5img class="anchor" src="icons/tick.png" id="cap_comm"\ 6lemma cap_comm : ∀U.∀A,B:U →Prop. 
82   A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
83 #U #A #B #a % * /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed. 
84
85 \ 5img class="anchor" src="icons/tick.png" id="union_idemp"\ 6lemma union_idemp: ∀U.∀A:U →Prop. 
86   A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
87 #U #A #a % [* // | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] qed. 
88
89 \ 5img class="anchor" src="icons/tick.png" id="cap_idemp"\ 6lemma cap_idemp: ∀U.∀A:U →Prop. 
90   A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A.
91 #U #A #a % [* // | /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] qed. 
92
93 (*distributivities *)
94
95 \ 5img class="anchor" src="icons/tick.png" id="distribute_intersect"\ 6lemma distribute_intersect : ∀U.∀A,B,C:U→Prop. 
96   (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B) \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (B \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 C).
97 #U #A #B #C #w % [* * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
98 qed.
99   
100 \ 5img class="anchor" src="icons/tick.png" id="distribute_substract"\ 6lemma distribute_substract : ∀U.∀A,B,C:U→Prop. 
101   (A \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 B) \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (A \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C) \ 5a title="union" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 (B \ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 C).
102 #U #A #B #C #w % [* * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ | * * /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/] 
103 qed.
104
105 (* substraction *)
106 \ 5img class="anchor" src="icons/tick.png" id="substract_def"\ 6lemma substract_def:∀U.∀A,B:U→Prop. A\ 5a title="substraction" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6\ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 A \ 5a title="intersection" href="cic:/fakeuri.def(1)"\ 6\ 5/a\ 6 \ 5a title="complement" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6B.
107 #U #A #B #w normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
108 qed.