@[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.14}) (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.