Аналіз I, Глава 3.2

У цій главі ми пропонуємо версію теорії множин Цермело-Франкеля (з атомами), яка намагається максимально точно наслідувати оригінальний тексту Аналізу I, Глава 3.2. Вся нумерація посилається на оригінальний текст.

Я (пр.перекл. Терренс Тао) намагався зробити переклад якомога точнішим перефразуванням оригінального тексту. Коли є вибір між більш ідіоматичним рішенням Lean та більш точним перекладом, я зазвичай обирав останній. Зокрема, будуть місця, де код Lean можна було б "підбуцнути", щоб зробити його більш елегантним та ідіоматичним, але я свідомо уникав цього вибору.

Цей розділ переважно необов'язковий, хоча в ньому чітко зазначено аксіому регулярності, яка використовується в другорядній ролі у вправі в розділі 3.5.

Основні конструкції та результати цього розділу:

• Парадокс Рассела (виключення аксіоми універсальної специфікації)
• Аксіома регулярності - аксіома, розроблена для уникнення парадоксу Рассела

@[reducible, inline]

abbrev Chapter3.axiom_of_universal_specification [SetTheory] : Prop

Аксіома 3.8 (Універсальне визначення)

Equations

• Chapter3.axiom_of_universal_specification = ∀ (P : Chapter3.Object → Prop), ∃ (A : Chapter3.Set), ∀ (x : Chapter3.Object), x ∈ A ↔ P x

theorem Chapter3.Russells_paradox [SetTheory] : ¬axiom_of_universal_specification

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

Аксіома 3.9 (Регулярність )

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

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи порожньої множини.

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

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи сінглетона.

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₂

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи пари.

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

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела чи операції об'єднання.

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⟩

Вправа 3.2.1. Дух цієї вправи полягає в тому, щоб встановити ці результати без використання парадоксу Рассела, or the specify operation.

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

Вправа 3.2.1. The spirit of the exercise is to establish these results without using either Russell's paradox, or the specify operation.

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

Вправа 3.2.2

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

Вправа 3.2.2

theorem Chapter3.SetTheory.Set.univ_imp [SetTheory] (U : Set) (hU : ∀ (x : Object), x ∈ U) : axiom_of_universal_specification

Вправа 3.2.3

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

Вправа 3.2.3