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".
14 (**** a subset of A is just an object of type A→Prop ****)
16 definition empty_set ≝ λA:Type[0].λa:A.False.
17 notation "\emptyv" non associative with precedence 90 for @{'empty_set}.
18 interpretation "empty set" 'empty_set = (empty_set ?).
20 definition singleton ≝ λA.λx,a:A.x=a.
21 (* notation "{x}" non associative with precedence 90 for @{'sing_lang $x}. *)
22 interpretation "singleton" 'singl x = (singleton ? x).
24 definition union : ∀A:Type[0].∀P,Q.A → Prop ≝ λA,P,Q,a.P a ∨ Q a.
25 interpretation "union" 'union a b = (union ? a b).
27 definition intersection : ∀A:Type[0].∀P,Q.A→Prop ≝ λA,P,Q,a.P a ∧ Q a.
28 interpretation "intersection" 'intersects a b = (intersection ? a b).
30 definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a).
31 interpretation "subset" 'subseteq a b = (intersection ? a b).
33 (* extensional equality *)
34 definition eqP ≝ λA:Type[0].λP,Q:A → Prop.∀a:A.P a ↔ Q a.
35 notation "A =1 B" non associative with precedence 45 for @{'eqP $A $B}.
36 interpretation "extensional equality" 'eqP a b = (eqP ? a b).
38 lemma eqP_sym: ∀U.∀A,B:U →Prop.
40 #U #A #B #eqAB #a @iff_sym @eqAB qed.
42 lemma eqP_trans: ∀U.∀A,B,C:U →Prop.
43 A =1 B → B =1 C → A =1 C.
44 #U #A #B #C #eqAB #eqBC #a @iff_trans // qed.
46 lemma eqP_union_r: ∀U.∀A,B,C:U →Prop.
47 A =1 C → A ∪ B =1 C ∪ B.
48 #U #A #B #C #eqAB #a @iff_or_r @eqAB qed.
50 lemma eqP_union_l: ∀U.∀A,B,C:U →Prop.
51 B =1 C → A ∪ B =1 A ∪ C.
52 #U #A #B #C #eqBC #a @iff_or_l @eqBC qed.
55 lemma union_comm : ∀U.∀A,B:U →Prop.
57 #U #A #B #a % * /2/ qed.
59 lemma union_assoc: ∀U.∀A,B,C:U → Prop.
60 A ∪ B ∪ C =1 A ∪ (B ∪ C).
61 #S #A #B #C #w % [* [* /3/ | /3/] | * [/3/ | * /3/]
64 lemma cap_comm : ∀U.∀A,B:U →Prop.
66 #U #A #B #a % * /2/ qed.
68 lemma union_idemp: ∀U.∀A:U →Prop.
70 #U #A #a % [* // | /2/] qed.
72 lemma cap_idemp: ∀U.∀A:U →Prop.
74 #U #A #a % [* // | /2/] qed.