matita/contribs/dama/dama/classical_pointwise/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
  16
  17 include "nat/nat.ma".
  18 include "logic/connectives.ma".
  19
  20
  21 definition set   ≝   λX:Type.X → Prop.
  22
  23 definition member_of : ∀X.set X → X → Prop≝ λX.λA:set X.λx.A x.
  24
  25 notation "hvbox(x break ∈ A)" with precedence 60
  26 for @{ 'member_of $x $A }.
  27
  28 interpretation "Member of" 'member_of x A =
  29  (cic:/matita/classical_pointwise/sets/member_of.con _ A x).
  30
  31 notation "hvbox(x break ∉ A)" with precedence 60
  32 for @{ 'not_member_of $x $A }.
  33
  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)).
  37
  38 definition emptyset : ∀X.set X ≝  λX:Type.λx:X.False.
  39
  40 notation "∅︀" with precedence 100 for @{ 'emptyset }.
  41
  42 interpretation "Emptyset" 'emptyset =
  43  (cic:/matita/classical_pointwise/sets/emptyset.con _).
  44
  45 definition subset: ∀X. set X → set X → Prop≝ λX.λA,B:set X.∀x. x ∈ A → x ∈ B.
  46
  47 notation "hvbox(A break ⊆ B)" with precedence 60
  48 for @{ 'subset $A $B }.
  49
  50 interpretation "Subset" 'subset A B =
  51  (cic:/matita/classical_pointwise/sets/subset.con _ A B).
  52
  53 definition intersection: ∀X. set X → set X → set X ≝
  54  λX.λA,B:set X.λx. x ∈ A ∧ x ∈ B.
  55
  56 notation "hvbox(A break ∩ B)" with precedence 70
  57 for @{ 'intersection $A $B }.
  58
  59 interpretation "Intersection" 'intersection A B =
  60  (cic:/matita/classical_pointwise/sets/intersection.con _ A B).
  61
  62 definition union: ∀X. set X → set X → set X ≝ λX.λA,B:set X.λx. x ∈ A ∨ x ∈ B.
  63
  64 notation "hvbox(A break ∪ B)" with precedence 65
  65 for @{ 'union $A $B }.
  66
  67 interpretation "Union" 'union A B =
  68  (cic:/matita/classical_pointwise/sets/union.con _ A B).
  69
  70 definition seq ≝ λX:Type.nat → X.
  71
  72 definition nth ≝  λX.λA:seq X.λi.A i.
  73
  74 notation "hvbox(A \sub i)" with precedence 100
  75 for @{ 'nth $A $i }.
  76
  77 interpretation "nth" 'nth A i =
  78  (cic:/matita/classical_pointwise/sets/nth.con _ A i).
  79
  80 definition countable_union: ∀X. seq (set X) → set X ≝
  81  λX.λA:seq (set X).λx.∃j.x ∈ A \sub j.
  82
  83 notation "∪ \sub (ident i opt (: ty)) B" with precedence 65
  84 for @{ 'big_union ${default @{(λ${ident i}:$ty.$B)} @{(λ${ident i}.$B)}}}.
  85
  86 interpretation "countable_union" 'big_union η.t =
  87  (cic:/matita/classical_pointwise/sets/countable_union.con _ t).
  88
  89 definition complement: ∀X. set X \to set X ≝ λX.λA:set X.λx. x ∉ A.
  90
  91 notation "A \sup 'c'" with precedence 100
  92 for @{ 'complement $A }.
  93
  94 interpretation "Complement" 'complement A =
  95  (cic:/matita/classical_pointwise/sets/complement.con _ A).
  96
  97 definition inverse_image: ∀X,Y.∀f: X → Y.set Y → set X ≝
  98  λX,Y,f,B,x. f x ∈ B.
  99
 100 notation "hvbox(f \sup (-1))" with precedence 100
 101 for @{ 'finverse $f }.
 102
 103 interpretation "Inverse image" 'finverse f =
 104  (cic:/matita/classical_pointwise/sets/inverse_image.con _ _ f).