Library Coqtail.Topology.Sets


Section Sets.
  Variable U : Type.

  Definition set := UProp.

  Definition In (A:set) x : Prop := A x.

  Definition Set_included A B := x, In A xIn B x.

  Inductive Set_inter (A B:set) : set :=
    Set_inter_intro : x, In A xIn B xIn (Set_inter A B) x.

  Inductive Set_union (A B:set) : set :=
    | Set_union_intro_l : x, In A xIn (Set_union A B) x
    | Set_union_intro_r : x, In B xIn (Set_union A B) x.

  Inductive Set_empty : set :=.

  Inductive Set_full : set :=
    | Set_full_intro : x, In Set_full x.

  Inductive Set_singleton (x:U) : set :=
    Set_singleton_intro : In (Set_singleton x) x.

  Inductive Set_couple (x y:U) : set :=
    | Set_couple_l : In (Set_couple x y) x
    | Set_couple_r : In (Set_couple x y) y.

  Inductive Set_triple (x y z:U) : set :=
    | Set_triple_l : In (Set_triple x y z) x
    | Set_triple_m : In (Set_triple x y z) y
    | Set_triple_r : In (Set_triple x y z) z.

  Definition Set_complement (A:set) : set := fun x:U¬ In A x.

  Definition Set_minus (B C:set) : set := fun x:UIn B x ¬ In C x.

  Definition Set_subtract (B:set) (x:U) : set := Set_minus B (Set_singleton x).

  Inductive Set_disjoint (B C:set) : Prop :=
    Set_disjoint_intro : ( x:U, ¬ In (Set_inter B C) x) → Set_disjoint B C.

  Inductive Set_inhabited (B:set) : Prop :=
    Inhabited_intro : x:U, In B xSet_inhabited B.

  Definition Set_strict_included (B C:set) : Prop := Set_included B C B C.

  Definition Set_same (B C:set) : Prop := Set_included B C Set_included C B.

  Axiom Set_Extensionality : A B:set, Set_same A BA = B.
End Sets.

Implicit Arguments set [U].
Implicit Arguments In [U].
Implicit Arguments Set_included [U].
Implicit Arguments Set_inter [U].
Implicit Arguments Set_union [U].
Implicit Arguments Set_empty [U].
Implicit Arguments Set_full [U].
Implicit Arguments Set_singleton [U].
Implicit Arguments Set_couple [U].
Implicit Arguments Set_triple [U].
Implicit Arguments Set_complement [U].
Implicit Arguments Set_minus [U].
Implicit Arguments Set_subtract [U].
Implicit Arguments Set_disjoint [U].
Implicit Arguments Set_inhabited [U].
Implicit Arguments Set_strict_included [U].
Implicit Arguments Set_same [U].
Implicit Arguments Set_Extensionality [U].