Sets
Definition set : Type := A → Prop.
Definition empty_set : set := fun _ ⇒ False.
Definition full_set : set := fun _ ⇒ True.
Definition is_full_set(P : set) : Prop := ∀(a : A), P a.
Definition add(a : A)(P : set) : set := fun(b : A) ⇒ a = b ∨ P b.
Definition subset(P Q : set) : Prop := ∀(a : A), P a → Q a.
Definition union(P Q : set) : set := fun(a : A) ⇒ P a ∨ Q a.
Definition intersection(P Q : set) : set := fun(a : A) ⇒ P a ∧ Q a.
Definition set_inverse(P : set) : set := fun(a : A) ⇒ ¬ (P a).
Lemma subset_refl : ∀(P : set), subset P P.
Lemma subset_trans : ∀(P1 P2 P3 : set),
subset P1 P2 → subset P2 P3 → subset P1 P3.
Lemma subset_add : ∀(P : set)(a : A), subset P (add a P).
Lemma subset_union_left : ∀(P Q : set), subset P (union P Q).
Lemma subset_union_right : ∀(P Q : set), subset Q (union P Q).
Lemma subset_union_both : ∀(P1 P2 Q1 Q2 : set),
subset P1 Q1 → subset P2 Q2 → subset (union P1 P2) (union Q1 Q2).
Lemma subset_union_lub : ∀(P1 P2 Q : set),
subset P1 Q → subset P2 Q → subset (union P1 P2) Q.
Definition set_equal(P Q : set) : Prop :=
∀(a : A), P a ↔ Q a.
Lemma set_equal_refl : ∀(P : set), set_equal P P.
Lemma set_equal_symm : ∀(P Q : set),
set_equal Q P → set_equal P Q.
Lemma set_equal_trans : ∀(P1 P2 P3 : set),
set_equal P1 P2 → set_equal P2 P3 → set_equal P1 P3.
Lemma set_equal_subset_char : ∀(P Q : set),
set_equal P Q ↔ (subset P Q ∧ subset Q P).
Lemma set_equal_subset : ∀(P1 P2 : set)(Q1 Q2 : set),
set_equal P1 P2 →
set_equal Q1 Q2 →
subset P1 Q1 →
subset P2 Q2.
Lemma union_comm : ∀(P Q : set),
set_equal (union P Q) (union Q P).
Lemma set_equal_union : ∀(P1 P2 Q1 Q2 : set),
set_equal P1 Q1 →
set_equal P2 Q2 →
set_equal (union P1 P2) (union Q1 Q2).
Lemma set_equal_intersection : ∀(P1 P2 Q1 Q2 : set),
set_equal P1 Q1 →
set_equal P2 Q2 →
set_equal (intersection P1 P2) (intersection Q1 Q2).
Lemma set_equal_set_inverse : ∀(P Q : set),
set_equal P Q → set_equal (set_inverse P) (set_inverse Q).
Lemma set_equal_is_full : ∀(P Q : set),
set_equal P Q →
is_full_set P →
is_full_set Q.
Lemma set_equal_union_subset_right : ∀(P Q : set),
subset Q P → set_equal (union P Q) P.
Lemma subset_empty_set : ∀(P : set), subset empty_set P.
Lemma set_equal_union_empty_right : ∀(P Q : set),
set_equal Q empty_set → set_equal (union P Q) P.
Lemma set_equal_implies_subset : ∀(P Q : set),
set_equal P Q → subset P Q.
Lemma set_equal_rw_r : ∀(P1 P2 P3 : set),
set_equal P2 P3 → set_equal P1 P3 → set_equal P1 P2.
Lemma intersection_complement : ∀(P : set)(a : A),
not (intersection P (set_inverse P) a).
Lemma set_inverse_intersection : ∀(P Q : set)(a : A),
union (set_inverse P) (set_inverse Q) a →
set_inverse (intersection P Q) a.
Lemma double_set_inverse : ∀(P : set)(a : A),
P a → set_inverse (set_inverse P) a.
Lemma full_set_full : is_full_set full_set.
Lemma full_subset_full :
∀(P : set), subset full_set P → is_full_set P.
End Sets.
Implicit Arguments is_full_set [A].
Implicit Arguments add [A].
Implicit Arguments subset [A].
Implicit Arguments union [A].
Implicit Arguments intersection [[A]].
Implicit Arguments set_inverse [[A]].
Implicit Arguments set_equal [A].
Definition sets_containing{A : Type}(a : A) : set (set A) :=
fun(s : set A) ⇒ s a.