2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/logic.ma".
13 include "basics/core_notation/singl_1.ma".
15 (**** a subset of A is just an object of type A→Prop ****)
17 definition empty_set ≝ λA:Type[0].λa:A.False.
18 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
19 interpretation "empty set" 'empty_set = (empty_set ?).
21 definition singleton ≝ λA.λx,a:A.x=a.
22 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
23 interpretation "singleton" 'singl x = (singleton ? x).
25 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
26 interpretation "union" 'union a b = (union ? a b).
28 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
29 interpretation "intersection" 'intersects a b = (intersection ? a b).
31 definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
32 interpretation "complement" 'not a = (complement ? a).
34 definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
35 interpretation "substraction" 'minus a b = (substraction ? a b).
37 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
38 interpretation "subset" 'subseteq a b = (subset ? a b).
40 (* extensional equality *)
41 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
42 (* ≐ is typed as \doteq *)
43 notation "A ≐ B" non associative with precedence 45 for @{'eqP $A $B}.
44 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
46 lemma eqP_sym: ∀U.∀A,B:U →Prop.
48 #U #A #B #eqAB #a @iff_sym @eqAB qed.
50 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
51 A ≐ B → B ≐ C → A ≐ C.
52 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
54 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
55 A ≐ C → A ∪ B ≐ C ∪ B.
56 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
58 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
59 B ≐ C → A ∪ B ≐ A ∪ C.
60 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
62 lemma eqP_intersect_r: ∀U.∀A,B,C:U →Prop.
63 A ≐ C → A ∩ B ≐ C ∩ B.
64 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
66 lemma eqP_intersect_l: ∀U.∀A,B,C:U →Prop.
67 B ≐ C → A ∩ B ≐ A ∩ C.
68 #U #A #B #C #eqBC #a @iff_and_l @eqBC qed.
70 lemma eqP_substract_r: ∀U.∀A,B,C:U →Prop.
71 A ≐ C → A - B ≐ C - B.
72 #U #A #B #C #eqAB #a @iff_and_r @eqAB qed.
74 lemma eqP_substract_l: ∀U.∀A,B,C:U →Prop.
75 B ≐ C → A - B ≐ A - C.
76 #U #A #B #C #eqBC #a @iff_and_l /2/ qed.
79 lemma union_empty_r: ∀U.∀A:U→Prop.
81 #U #A #w % [* // normalize #abs @False_ind /2/ | /2/]
84 lemma union_comm : ∀U.∀A,B:U →Prop.
86 #U #A #B #a % * /2/ qed.
88 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
89 A ∪ B ∪ C ≐ A ∪ (B ∪ C).
90 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
93 lemma cap_comm : ∀U.∀A,B:U →Prop.
95 #U #A #B #a % * /2/ qed.
97 lemma union_idemp: ∀U.∀A:U →Prop.
99 #U #A #a % [* // | /2/] qed.
101 lemma cap_idemp: ∀U.∀A:U →Prop.
103 #U #A #a % [* // | /2/] qed.
105 (*distributivities *)
107 lemma distribute_intersect : ∀U.∀A,B,C:U→Prop.
108 (A ∪ B) ∩ C ≐ (A ∩ C) ∪ (B ∩ C).
109 #U #A #B #C #w % [* * /3/ | * * /3/]
112 lemma distribute_substract : ∀U.∀A,B,C:U→Prop.
113 (A ∪ B) - C ≐ (A - C) ∪ (B - C).
114 #U #A #B #C #w % [* * /3/ | * * /3/]
118 lemma substract_def:∀U.∀A,B:U→Prop. A-B ≐ A ∩ ¬B.
119 #U #A #B #w normalize /2/