+(* In this Chapter we shall develop a naif theory of sets represented as characteristic
+predicates over some universe \ 5code\ 6A\ 5/code\ 6, that is as objects of type A→Prop *)
+
include "basics/logic.ma".
-(**** a subset of A is just an object of type A→Prop ****)
+(**** For instance the empty set is defined by the always function predicate *)
-definition empty_set ≝ λA:Type[0].λa:A.False.
+definition empty_set ≝ λA:Type[0].λa:A.\ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6.
notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
interpretation "empty set" 'empty_set = (empty_set ?).
-definition singleton ≝ λA.λx,a:A.x=a.
+(* Similarly, a singleton set contaning containing an element a, is defined
+by by the characteristic function asserting equality with a *)
+
+definition singleton ≝ λA.λx,a:A.x\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6a.
(* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
interpretation "singleton" 'singl x = (singleton ? x).
-definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
+(* The operations of union, intersection, complement and substraction
+are easily defined in terms of the propositional connectives of dijunction,
+conjunction and negation *)
+
+definition 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.
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.
+definition 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.
interpretation "intersection" 'intersects a b = (intersection ? a b).
-definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w.
+definition complement ≝ λU:Type[0].λA:U → Prop.λw.\ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 A w.
interpretation "complement" 'not a = (complement ? a).
-definition substraction := λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w.
+definition 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.
interpretation "substraction" 'minus a b = (substraction ? a b).
+(* Finally, we use implication to define the inclusion relation between
+sets *)
+
definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
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.
+(* Two sets are equals if and only if they have the same elements, that is,
+if the two characteristic functions are extensionally equivalent: *)
+
+definition 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.
notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
interpretation "extensional equality" 'eqP a b = (eqP ? a b).
+(* This notion of equality is different from the intensional equality of
+fucntions, hence we have to prove the usual properties: *)
+
lemma eqP_sym: ∀U.∀A,B:U →Prop.
- A =1 B → B =1 A.
+ A \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 B → B \ 5a title="extensional equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 61 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.
#U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
-lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
+(* For the same reason, we must also prove that all the operations we have
+ lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
A =1 C → A ∪ B =1 C ∪ B.
#U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
projects / helm.git / blobdiff