Documentation

Analysis.Section_3_2

source
@[reducible, inline]
abbrev Chapter3.axiom_of_universal_specification [SetTheory] :
Prop

Axiom 3.8 (Universal specification)

Equations
Instances For
    source
    theorem Chapter3.Russells_paradox [SetTheory] :
    ¬axiom_of_universal_specification
    source
    theorem Chapter3.SetTheory.Set.axiom_of_regularity [SetTheory] {A : Set} (h : A ≠ ∅) :
    ∃ (x : A.toSubtype), ∀ (S : Set), ↑x = set_to_object S → Disjoint S A

    Axiom 3.9 (Regularity)

    source
    theorem Chapter3.SetTheory.Set.emptyset_exists [SetTheory] (h : axiom_of_universal_specification) :
    ∃ (X : Set), ∀ (x : Object), x ∉ X

    Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the empty set.

    source
    theorem Chapter3.SetTheory.Set.singleton_exists [SetTheory] (h : axiom_of_universal_specification) (x : Object) :
    ∃ (X : Set), ∀ (y : Object), y ∈ X ↔ y = x

    Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the singleton set.

    source
    theorem Chapter3.SetTheory.Set.pair_exists [SetTheory] (h : axiom_of_universal_specification) (x₁ x₂ : Object) :
    ∃ (X : Set), ∀ (y : Object), y ∈ X ↔ y = x₁ ∨ y = x₂

    Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the pair set.

    source
    theorem Chapter3.SetTheory.Set.union_exists [SetTheory] (h : axiom_of_universal_specification) (A B : Set) :
    ∃ (Z : Set), ∀ (z : Object), z ∈ Z ↔ z ∈ A ∨ z ∈ B

    Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the union operation.

    source
    theorem Chapter3.SetTheory.Set.specify_exists [SetTheory] (h : axiom_of_universal_specification) (A : Set) (P : A.toSubtype → Prop) :
    ∃ (Z : Set), ∀ (z : Object), z ∈ Z ↔ ∃ (h : z ∈ A), P ⟨z, h⟩

    Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the specify operation.

    source
    theorem Chapter3.SetTheory.Set.replace_exists [SetTheory] (h : axiom_of_universal_specification) (A : Set) (P : A.toSubtype → Object → Prop) (hP : ∀ (x : A.toSubtype) (y y' : Object), P x y ∧ P x y' → y = y') :
    ∃ (Z : Set), ∀ (y : Object), y ∈ Z ↔ ∃ (a : A.toSubtype), P a y

    Exercise 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the replace operation.

    source
    theorem Chapter3.SetTheory.Set.not_mem_self [SetTheory] (A : Set) :
    set_to_object A ∉ A

    Exercise 3.2.2 (no set contains itself)

    source
    theorem Chapter3.SetTheory.Set.not_mem_mem [SetTheory] (A B : Set) :
    set_to_object A ∉ B ∨ set_to_object B ∉ A

    Exercise 3.2.2 (no two sets contain each other)

    source
    theorem Chapter3.SetTheory.Set.univ_iff [SetTheory] :
    axiom_of_universal_specification ↔ ∃ (U : Set), ∀ (x : Object), x ∈ U

    Exercise 3.2.3 (universal specification)

    source
    theorem Chapter3.SetTheory.Set.no_univ [SetTheory] :
    ¬∃ (U : Set), ∀ (x : Object), x ∈ U

    Exercise 3.2.3 (there is no universal set)