1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
18 include "logic/connectives.ma".
21 definition set ≝ λX:Type.X → Prop.
23 definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x.
25 notation "hvbox(x break ∈ A)" with precedence 60
26 for @{ 'member_of $x $A }.
28 interpretation "Member of" 'member_of x A =
29 (cic:/matita/classical_pointwise/sets/member_of.con _ A x).
31 notation "hvbox(x break ∉ A)" with precedence 60
32 for @{ 'not_member_of $x $A }.
34 interpretation "Not member of" 'not_member_of x A =
35 (cic:/matita/logic/connectives/Not.con
36 (cic:/matita/classical_pointwise/sets/member_of.con _ A x)).
38 definition emptyset : ∀X.set X ≝ λX:Type.λx:X.False.
40 notation "∅︀" with precedence 100 for @{ 'emptyset }.
42 interpretation "Emptyset" 'emptyset =
43 (cic:/matita/classical_pointwise/sets/emptyset.con _).
45 definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
47 notation "hvbox(A break ⊆ B)" with precedence 60
48 for @{ 'subset $A $B }.
50 interpretation "Subset" 'subset A B =
51 (cic:/matita/classical_pointwise/sets/subset.con _ A B).
53 definition intersection: ∀X. set X → set X → set X ≝
54 λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
56 notation "hvbox(A break ∩ B)" with precedence 70
57 for @{ 'intersection $A $B }.
59 interpretation "Intersection" 'intersection A B =
60 (cic:/matita/classical_pointwise/sets/intersection.con _ A B).
62 definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
64 notation "hvbox(A break ∪ B)" with precedence 65
65 for @{ 'union $A $B }.
67 interpretation "Union" 'union A B =
68 (cic:/matita/classical_pointwise/sets/union.con _ A B).
70 definition seq ≝ λX:Type.nat → X.
72 definition nth ≝ λX.λA:seq X.λi.A i.
74 notation "hvbox(A \sub i)" with precedence 100
77 interpretation "nth" 'nth A i =
78 (cic:/matita/classical_pointwise/sets/nth.con _ A i).
80 definition countable_union: ∀X. seq (set X) → set X ≝
81 λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
83 notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
84 for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
86 interpretation "countable_union" 'big_union η.t =
87 (cic:/matita/classical_pointwise/sets/countable_union.con _ t).
89 definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
91 notation "A \sup 'c'" with precedence 100
92 for @{ 'complement $A }.
94 interpretation "Complement" 'complement A =
95 (cic:/matita/classical_pointwise/sets/complement.con _ A).
97 definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
100 notation "hvbox(f \sup (-1))" with precedence 100
101 for @{ 'finverse $f }.
103 interpretation "Inverse image" 'finverse f =
104 (cic:/matita/classical_pointwise/sets/inverse_image.con _ _ f).