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

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

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

• Огляд типу залежного добутку Mathlib ?m.1 → sorry : Sort (imax ?u.374673 u_1)∀ α, Unknown identifier `X`X α.

• Аксіома вибору в різних еквівалентних формах, а також її рахункова версія.

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

namespace Chapter8 def product_zero_equiv {X: Fin 0 → Type} : (∀ i:Fin 0, X i) ≃ PUnit := { toFun f := PUnit.unit invFun x i := nomatch i left_inv f := byX:Fin 0 → Typef:(i : Fin 0) → X i⊢ (fun x i => nomatch i) ((fun f => PUnit.unit) f) = f aesopAll goals completed! 🐙 right_inv f := rfl }def product_one_equiv {X: Fin 1 → Type} : (∀ i:Fin 1, X i) ≃ X 0 := { toFun f := f 0 invFun x i := byX:Fin 1 → Typex:X 0i:Fin 1⊢ X i rwa [←Fin.fin_one_eq_zero i]X:Fin 1 → Typei:Fin 1x:X i⊢ X i at x left_inv f := byX:Fin 1 → Typef:(i : Fin 1) → X i⊢ (fun x i => ⋯.mp x) ((fun f => f 0) f) = f ext ihX:Fin 1 → Typef:(i : Fin 1) → X ii:Fin 1⊢ (fun x i => ⋯.mp x) ((fun f => f 0) f) i = f i; rw [Fin.fin_one_eq_zero i]hX:Fin 1 → Typef:(i : Fin 1) → X ii:Fin 1⊢ (fun x i => ⋯.mp x) ((fun f => f 0) f) 0 = f 0; simpAll goals completed! 🐙 right_inv f := rfl }def product_two_equiv {X: Fin 2 → Type} : (∀ i:Fin 2, X i) ≃ (X 0 × X 1) := { toFun f := (f 0, f 1) invFun f i := match i with | 0 => f.1 | 1 => f.2 left_inv f := byX:Fin 2 → Typef:(i : Fin 2) → X i⊢ (fun f i => match i with | 0 => f.1 | 1 => f.2) ((fun f => (f 0, f 1)) f) = f aesopAll goals completed! 🐙 right_inv f := rfl }def product_three_equiv {X: Fin 3 → Type} : (∀ i:Fin 3, X i) ≃ (X 0 × X 1 × X 2) := { toFun f := (f 0, f 1, f 2) invFun f i := match i with | 0 => f.1 | 1 => f.2.1 | 2 => f.2.2 left_inv f := byX:Fin 3 → Typef:(i : Fin 3) → X i⊢ (fun f i => match i with | 0 => f.1 | 1 => f.2.1 | 2 => f.2.2) ((fun f => (f 0, f 1, f 2)) f) = f aesopAll goals completed! 🐙 right_inv f := rfl } theorem axiom_of_countable_choice {I: Type} {X: I → Type} [Countable I] (h : ∀ i, Nonempty (X i)) : Nonempty (∀ i, X i) := axiom_of_choice h end Chapter8