Analysis I, Section 8.4: The axiom of choice

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

• Review of Mathlib's dependent product type ?m.1 → sorry : Sort (imax ?u.374673 u_1)∀ α, Unknown identifier `X`X α.

• The axiom of choice in various equivalent forms, as well as the countable axiom of choice.

As the Chapter 3 set theory has been deprecated for many chapters at this point, we will not insert the axiom of choice directly into that theory in this text; but this could be accomplished if desired (e.g., by extending the Unknown identifier `Chapter3.SetTheory`Chapter3.SetTheory class to a Unknown identifier `Chapter3.SetTheoryWithChoice`Chapter3.SetTheoryWithChoice class), and students are welcome to attempt this separately. Instead, we will use Mathlib's native Classical.choice.{u} {α : Sort u} : Nonempty α → αClassical.choice axiom. Technically, this axiom has already been used quite frequently in the text already, in large part because Mathlib uses Classical.choice.{u} {α : Sort u} : Nonempty α → αClassical.choice to derive many weaker statements, such as the law of the excluded middle. So the distinctions made in the original text regarding whether a given statement or not uses the axiom of choice are somewhat blurred in this formalization. It is theoretically possible to restore this distinction by removing the reliance on Mathlib and working throughout with custom structures such as Unknown identifier `Chapter3.SetTheory`Chapter3.SetTheory and Unknown identifier `Chapter3.SetTheoryWithChoice`Chapter3.SetTheoryWithChoice, but this would be extremely tedious and not attempted here.

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