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 ∀ α, 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 Chapter3.SetTheory class to a Chapter3.SetTheoryWithChoice class), and students are welcome to attempt this separately. Instead, we will use Mathlib's native Classical.choice axiom. Technically, this axiom has already been used quite frequently in the text already, in large part because Mathlib uses 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 Chapter3.SetTheory and Chapter3.SetTheoryWithChoice, but this would be extremely tedious and not attempted here.

@[reducible, inline]

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

Definition 8.4.1 (Infinite Cartesian products). We will avoid using this definition in favor of the Mathlib form ∀ α, X α which we will shortly show is equivalent to (or more precisely, generalizes) this one.

Because Lean does not allow unrestricted unions of types, we cheat slightly here by assuming all the X α are sets in a common universe U. Note that the Mathlib definition does not have this restriction.

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 α))

Equivalence with Mathlib's product

Equations

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

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

Example 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)

Axiom 8.1 (Choice)

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))

Lemma 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))

Remark 8.4.6. This special case of Lemma 8.4.5 avoids (countable) choice.

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)

Proposition 8.4.7 / Exercise 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)

Exercise 8.4.1. The spirit of the question here is to establish this result directly from exists_function, avoiding previous results that relied more explicitly on the axiom of choice.

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

Exercise 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)

Exercise 8.4.2. The spirit of the question here is to establish this result directly from exists_set_singleton_intersect, avoiding previous results that relied more explicitly on the axiom of choice.

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

Exercise 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)

Exercise 8.4.3. The spirit of the question here is to establish this result directly from Function.Injective.inv_surjective, avoiding previous results that relied more explicitly on the axiom of choice.