Аналіз I, Розділ 8.4: Аксіома вибору

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

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

• Огляд типу залежного добутку Mathlib ∀ α, X α.
• Аксіома вибору в різних еквівалентних формах, а також її рахункова версія.

Оскільки розділ 3, присвячений теорії множин, у багатьох місцях вже не використовується, ми не будемо вставляти аксіому вибору безпосередньо в цю теорію у цьому тексті; проте це можна зробити за бажання (наприклад, розширивши клас Chapter3.SetTheory до Chapter3.SetTheoryWithChoice), і студентам можна запропонувати зробити це окремо. Натомість ми використовуватимемо вбудовану в Mathlib аксіому Classical.choice. Технічно ця аксіома вже досить часто використовувалась у тексті, оскільки Mathlib використовує Classical.choice для виведення багатьох слабших тверджень, наприклад закону виключеного третього. Тож розмежування, зроблене в оригінальному тексті щодо того, чи використовує конкретне твердження аксіому вибору, у цій формалізації дещо розмито. Теоретично можна відновити це розмежування, прибравши залежність від Mathlib і працюючи з власними структурами типу Chapter3.SetTheory і Chapter3.SetTheoryWithChoice, але це було б дуже трудомістким і тут не розглядається.

@[reducible, inline]

abbrev Chapter8.CartesianProduct {I U : Type} (X : I → Set U) : Type

Визначення 8.4.1 (Нескінченні декартові добутки). Ми уникатимемо використання цієї дефініції на користь форми Mathlib ∀ α, X α, яка, як незабаром покажемо є еквівалентною (або, точніше, такою, що узагальнює) цю.

Оскільки Lean не дозволяє необмежених об'єднань типів, ми дещо обходимо це, припускаючи, що всі X α є підмножинами в спільній універсі U. Зауважте, що визначення в Mathlib не має цього обмеження.

Equations

• Chapter8.CartesianProduct X = { x : I → ↑(⋃ (α : I), X α) // ∀ (α : I), ↑(x α) ∈ X α }

def Chapter8.CartesianProduct.equiv {I U : Type} (X : I → Set U) : CartesianProduct X ≃ ((α : I) → ↑(X α))

Еквівалентність з добутком у Mathlib

Equations

• One or more equations did not get rendered due to their size.

def Chapter8.Function.equiv {I X : Type} : (I → X) ≃ (I → X)

Приклад 8.4.2.

Equations

• Chapter8.Function.equiv = { toFun := fun (f : I → X) => f, invFun := fun (f : I → X) => f, left_inv := ⋯, right_inv := ⋯ }

def Chapter8.product_zero_equiv {X : Fin 0 → Type} : ((i : Fin 0) → X i) ≃ PUnit.{u_1}

Equations

• Chapter8.product_zero_equiv = { toFun := fun (f : (i : Fin 0) → X i) => PUnit.unit, invFun := fun (x : PUnit.{?u.13}) (i : Fin 0) => nomatch i, left_inv := ⋯, right_inv := ⋯ }

def Chapter8.product_one_equiv {X : Fin 1 → Type} : ((i : Fin 1) → X i) ≃ X 0

Equations

• Chapter8.product_one_equiv = { toFun := fun (f : (i : Fin 1) → X i) => f 0, invFun := fun (x : X 0) (i : Fin 1) => ⋯.mp x, left_inv := ⋯, right_inv := ⋯ }

def Chapter8.product_two_equiv {X : Fin 2 → Type} : ((i : Fin 2) → X i) ≃ X 0 × X 1

Equations

• One or more equations did not get rendered due to their size.

def Chapter8.product_three_equiv {X : Fin 3 → Type} : ((i : Fin 3) → X i) ≃ X 0 × X 1 × X 2

Equations

• One or more equations did not get rendered due to their size.

theorem Chapter8.axiom_of_choice {I : Type} {X : I → Type} (h : ∀ (i : I), Nonempty (X i)) : Nonempty ((i : I) → X i)

Аксіома 8.1 (Аксіома вибору)

theorem Chapter8.axiom_of_countable_choice {I : Type} {X : I → Type} [Countable I] (h : ∀ (i : I), Nonempty (X i)) : Nonempty ((i : I) → X i)

theorem Chapter8.exist_tendsTo_sup {E : Set ℝ} (hnon : E.Nonempty) (hbound : BddAbove E) : ∃ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))

Лема 8.4.5

theorem Chapter8.exist_tendsTo_sup_of_closed {E : Set ℝ} (hnon : E.Nonempty) (hbound : BddAbove E) (hclosed : IsClosed E) : ∃ (a : ℕ → ℝ), (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))

Зауваження 8.4.6. Цей спеціальний випадок Леми 8.4.5 обходиться без (рахункової) аксіоми вибору.

theorem Chapter8.exists_function {X Y : Type} {P : X → Y → Prop} (h : ∀ (x : X), ∃ (y : Y), P x y) : ∃ (f : X → Y), ∀ (x : X), P x (f x)

Твердження 8.4.7 / Вправа 8.4.1

theorem Chapter8.axiom_of_choice_from_exists_function {I : Type} {X : I → Type} (h : ∀ (i : I), Nonempty (X i)) : Nonempty ((i : I) → X i)

Вправа 8.4.1. Сенс цього завдання — встановити цей результат прямо з exists_function, уникаючи попередніх результатів, що більш явно покладалися на аксіому вибору.

theorem Chapter8.exists_set_singleton_intersect {I U : Type} {X : I → Set U} (h : Set.univ.PairwiseDisjoint X) (hnon : ∀ (α : I), Nonempty ↑(X α)) : ∃ (Y : Set U), ∀ (α : I), Nat.card ↑(Y ∩ X α) = 1

Вправа 8.4.2

theorem Chapter8.axiom_of_choice_from_exists_set_singleton_intersect {I : Type} {X : I → Type} (h : ∀ (i : I), Nonempty (X i)) : Nonempty ((i : I) → X i)

Вправа 8.4.2. Сенс цього завдання — встановити цей результат прямо з exists_set_singleton_intersect, уникаючи попередніх результатів, що більш явно покладалися на аксіому вибору.

theorem Chapter8.Function.Injective.inv_surjective {A B : Type} {g : B → A} (hg : Function.Surjective g) : ∃ (f : A → B), Function.Injective f ∧ Function.RightInverse f g

Вправа 8.4.3

theorem Chapter8.axiom_of_choice_from_function_injective_inv_surjective {I : Type} {X : I → Type} (h : ∀ (i : I), Nonempty (X i)) : Nonempty ((i : I) → X i)

Вправа 8.4.3. Сенс цього завдання — встановити цей результат прямо з Function.Injective.inv_surjective, уникаючи попередніх результатів, що більш явно покладалися на аксіому вибору.