]> matita.cs.unibo.it Git - helm.git/blob - matita/dama/sets.ma
closed all axioms
[helm.git] / matita / dama / sets.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/sets/".
16
17 include "nat/nat.ma".
18
19 definition set   ≝   λX:Type.X → Prop.
20
21 definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x.
22
23 notation "hvbox(x break ∈ A)" with precedence 60
24 for @{ 'member_of $x $A }.
25
26 interpretation "Member of" 'member_of x A =
27  (cic:/matita/sets/member_of.con _ A x).
28  
29 notation "hvbox(x break ∉ A)" with precedence 60
30 for @{ 'not_member_of $x $A }.
31
32 interpretation "Not member of" 'not_member_of x A =
33  (cic:/matita/logic/connectives/Not.con
34   (cic:/matita/sets/member_of.con _ A x)).
35
36 definition emptyset : ∀X.set X ≝  λX:Type.λx:X.False.
37
38 notation "∅︀" with precedence 100 for @{ 'emptyset }.
39
40 interpretation "Emptyset" 'emptyset =
41  (cic:/matita/sets/emptyset.con _).
42
43 definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
44
45 notation "hvbox(A break ⊆ B)" with precedence 60
46 for @{ 'subset $A $B }.
47
48 interpretation "Subset" 'subset A B =
49  (cic:/matita/sets/subset.con _ A B).
50  
51 definition intersection: ∀X. set X → set X → set X ≝ 
52  λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
53
54 notation "hvbox(A break ∩ B)" with precedence 70
55 for @{ 'intersection $A $B }.
56
57 interpretation "Intersection" 'intersection A B =
58  (cic:/matita/sets/intersection.con _ A B).
59  
60 definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
61
62 notation "hvbox(A break ∪ B)" with precedence 65
63 for @{ 'union $A $B }.
64
65 interpretation "Union" 'union A B =
66  (cic:/matita/sets/union.con _ A B).
67
68 definition seq ≝ λX:Type.nat → X.
69
70 definition nth ≝  λX.λA:seq X.λi.A i.
71
72 notation "hvbox(A \sub i)" with precedence 100
73 for @{ 'nth $A $i }.
74
75 interpretation "nth" 'nth A i =
76  (cic:/matita/sets/nth.con _ A i).
77
78 definition countable_union: ∀X. seq (set X) → set X ≝ 
79  λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
80
81 notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
82 for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
83
84 interpretation "countable_union" 'big_union η.t =
85  (cic:/matita/sets/countable_union.con _ t).  
86
87 definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
88
89 notation "A \sup 'c'" with precedence 100
90 for @{ 'complement $A }.
91
92 interpretation "Complement" 'complement A =
93  (cic:/matita/sets/complement.con _ A).
94  
95 definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
96  λX,Y,f,B,x. f x ∈ B.
97
98 notation "hvbox(f \sup (-1))" with precedence 100
99 for @{ 'finverse $f }.
100
101 interpretation "Inverse image" 'finverse f =
102  (cic:/matita/sets/inverse_image.con _ _ f).