Analysis
8.4. The axiom of choice

Imports

import Mathlib.Tactic
import Analysis.Section_8_1
import Analysis.Section_8_2

set_option doc.verso.suggestions false

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.

namespace Chapter8

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.

abbrev CartesianProduct {I U: Type} (X : I → Set U) := { x : I → ⋃ α, X α // ∀ α, ↑(x α) ∈ X α }

Equivalence with Mathlib's product

def CartesianProduct.equiv {I U: Type} (X : I → Set U) :
  CartesianProduct X ≃ ∀ α, X α := {
  toFun x α := ⟨ x.val α, byI:TypeU:TypeX:I → Set Ux:CartesianProduct Xα:I⊢ ↑(↑x α) ∈ X α aesopAll goals completed! 🐙 ⟩
  invFun x := ⟨ fun α ↦ ⟨ x α, byI:TypeU:TypeX:I → Set Ux:(α : I) → ↑(X α)α:I⊢ ↑(x α) ∈ ⋃ α, X α simpI:TypeU:TypeX:I → Set Ux:(α : I) → ↑(X α)α:I⊢ ∃ i, ↑(x α) ∈ X i; use αhI:TypeU:TypeX:I → Set Ux:(α : I) → ↑(X α)α:I⊢ ↑(x α) ∈ X α; aesopAll goals completed! 🐙 ⟩, byI:TypeU:TypeX:I → Set Ux:(α : I) → ↑(X α)⊢ ∀ (α : I), ↑((fun α ↦ ⟨↑(x α), ⋯⟩) α) ∈ X α aesopAll goals completed! 🐙 ⟩
  left_inv x := byI:TypeU:TypeX:I → Set Ux:CartesianProduct X⊢ (fun x ↦ ⟨fun α ↦ ⟨↑(x α), ⋯⟩, ⋯⟩) ((fun x α ↦ ⟨↑(↑x α), ⋯⟩) x) = x aesopAll goals completed! 🐙
  right_inv x := byI:TypeU:TypeX:I → Set Ux:(α : I) → ↑(X α)⊢ (fun x α ↦ ⟨↑(↑x α), ⋯⟩) ((fun x ↦ ⟨fun α ↦ ⟨↑(x α), ⋯⟩, ⋯⟩) x) = x aesopAll goals completed! 🐙
  }

Example 8.4.2.

def Function.equiv {I X:Type} : (∀ _:I, X) ≃ (I → X) := {
  toFun f := f
  invFun f := f
  left_inv _f := rfl
  right_inv _f := rfl
}

              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
}

Axiom 8.1 (Choice)

theorem axiom_of_choice {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) :
  Nonempty (∀ i, X i) := byI:TypeX:I → Typeh:∀ (i : I), Nonempty (X i)⊢ Nonempty ((i : I) → X i) use fun i ↦ (h i).someAll goals completed! 🐙

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

Lemma 8.4.5

theorem exist_tendsTo_sup {E: Set ℝ} (hnon: E.Nonempty) (hbound: BddAbove E) :
  ∃ a : ℕ → ℝ, (∀ n, a n ∈ E) ∧ Filter.atTop.Tendsto a (nhds (sSup E)) := byE:Set ℝhnon:E.Nonemptyhbound:BddAbove E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
  -- This proof is written to follow the structure of the original text.
  set X : ℕ → Set ℝ := fun n ↦ { x ∈ E | sSup E - 1 / (n+1:ℝ) ≤ x ∧ x ≤ sSup E }E:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
  have hX : ∀ n, Nonempty (X n) := byE:Set ℝhnon:E.Nonemptyhbound:BddAbove E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
    intro nE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕ⊢ Nonempty ↑(X n)
    have : 1 / (n+1:ℝ) > 0 := byE:Set ℝhnon:E.Nonemptyhbound:BddAbove E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E)) positivityAll goals completed! 🐙
    choose s hs using (lt_csSup_iff hbound hnon).mp (show sSup E - 1 / (n+1:ℝ) < sSup E byE:Set ℝhnon:E.Nonemptyhbound:BddAbove E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E)) linarithAll goals completed! 🐙)
    use spropertyE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕthis:1 / (↑n + 1) > 0s:ℝhs:s ∈ E ∧ sSup E - 1 / (↑n + 1) < s⊢ s ∈ X n; simp_all [X]propertyE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕs:ℝthis:0 < ↑n + 1hs:s ∈ E ∧ sSup E - (↑n + 1)⁻¹ < s⊢ sSup E ≤ s + (↑n + 1)⁻¹ ∧ s ≤ sSup E
    refine ⟨ byE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕs:ℝthis:0 < ↑n + 1hs:s ∈ E ∧ sSup E - (↑n + 1)⁻¹ < s⊢ sSup E ≤ s + (↑n + 1)⁻¹ linarithAll goals completed! 🐙, le_csSup hbound hs.1 ⟩
  have ⟨ a ⟩ := axiom_of_countable_choice hXE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
  use fun n ↦ ↑(a n)hE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ (∀ (n : ℕ), (fun n ↦ ↑(a n)) n ∈ E) ∧ Filter.Tendsto (fun n ↦ ↑(a n)) Filter.atTop (nhds (sSup E)); constructorh.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ ∀ (n : ℕ), ↑(a n) ∈ Eh.rightE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun n ↦ ↑(a n)) Filter.atTop (nhds (sSup E)); swaph.rightE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun n ↦ ↑(a n)) Filter.atTop (nhds (sSup E))h.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ ∀ (n : ℕ), ↑(a n) ∈ E
  apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ sSup E - 1/(n+1:ℝ)) (h := fun _:ℕ ↦ sSup E)h.right.hgE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun n ↦ sSup E - 1 / (↑n + 1)) Filter.atTop (nhds (sSup E))h.right.hhE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun x ↦ sSup E) Filter.atTop (nhds (sSup E))h.right.hgfE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ (fun n ↦ sSup E - 1 / (↑n + 1)) ≤ fun n ↦ ↑(a n)h.right.hfhE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ (fun n ↦ ↑(a n)) ≤ fun x ↦ sSup Eh.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ ∀ (n : ℕ), ↑(a n) ∈ E
  .h.right.hgE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun n ↦ sSup E - 1 / (↑n + 1)) Filter.atTop (nhds (sSup E)) convert tendsto_const_nhds.sub (a := sSup E) (b := 0) _h.e'_1.h.e'_3E:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ sSup E = sSup E - 0h.right.hg.convert_4E:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun n ↦ 1 / (↑n + 1)) Filter.atTop (nhds 0); simph.right.hg.convert_4E:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun n ↦ 1 / (↑n + 1)) Filter.atTop (nhds 0)
    exact tendsto_one_div_add_atTop_nhds_zero_natAll goals completed! 🐙
  .h.right.hhE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)⊢ Filter.Tendsto (fun x ↦ sSup E) Filter.atTop (nhds (sSup E)) exact tendsto_const_nhdsAll goals completed! 🐙
  all_goals intro nh.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)n:ℕ⊢ ↑(a n) ∈ E; have := (a n).propertyh.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:(i : ℕ) → ↑(X i)n:ℕthis:↑(a n) ∈ X n⊢ ↑(a n) ∈ E; simp_all [X]All goals completed! 🐙

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

theorem exist_tendsTo_sup_of_closed {E: Set ℝ} (hnon: E.Nonempty) (hbound: BddAbove E) (hclosed: IsClosed E) :
  ∃ a : ℕ → ℝ, (∀ n, a n ∈ E) ∧ Filter.atTop.Tendsto a (nhds (sSup E)) := byE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
  set X : ℕ → Set ℝ := fun n ↦ { x ∈ E | sSup E - 1 / (n+1:ℝ) ≤ x ∧ x ≤ sSup E }E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
  have hX : ∀ n, Nonempty (X n) := byE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
    intro nE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕ⊢ Nonempty ↑(X n)
    have : 1 / (n+1:ℝ) > 0 := byE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E)) positivityAll goals completed! 🐙
    choose s hs using (lt_csSup_iff hbound hnon).mp (show sSup E - 1 / (n+1:ℝ) < sSup E byE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E)) linarithAll goals completed! 🐙)
    use spropertyE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕthis:1 / (↑n + 1) > 0s:ℝhs:s ∈ E ∧ sSup E - 1 / (↑n + 1) < s⊢ s ∈ X n; simp_all [X]propertyE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕs:ℝthis:0 < ↑n + 1hs:s ∈ E ∧ sSup E - (↑n + 1)⁻¹ < s⊢ sSup E ≤ s + (↑n + 1)⁻¹ ∧ s ≤ sSup E
    refine ⟨ byE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}n:ℕs:ℝthis:0 < ↑n + 1hs:s ∈ E ∧ sSup E - (↑n + 1)⁻¹ < s⊢ sSup E ≤ s + (↑n + 1)⁻¹ linarithAll goals completed! 🐙, le_csSup hbound hs.1 ⟩
  set a : ℕ → ℝ := fun n ↦ sInf (X n)E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
  have ha (n:ℕ) : a n ∈ X n := byE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed E⊢ ∃ a, (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E))
    apply IsClosed.csInf_mem _ Set.Nonempty.of_subtypeE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)n:ℕ⊢ BddBelow (X n)E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)n:ℕ⊢ IsClosed (X n)
    .E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)n:ℕ⊢ BddBelow (X n) rw [bddBelow_def]E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)n:ℕ⊢ ∃ x, ∀ y ∈ X n, x ≤ y; use sSup E - 1 / (n+1:ℝ)hE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)n:ℕ⊢ ∀ y ∈ X n, sSup E - 1 / (↑n + 1) ≤ y; aesopAll goals completed! 🐙
    .E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)n:ℕ⊢ IsClosed (X n) rw [show X n = E ∩ .Icc (sSup E - 1 / (n+1:ℝ)) (sSup E) by ext; aesop]E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)n:ℕ⊢ IsClosed (E ∩ Set.Icc (sSup E - 1 / (↑n + 1)) (sSup E))
      exact hclosed.inter isClosed_IccAll goals completed! 🐙
  use ahE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ (∀ (n : ℕ), a n ∈ E) ∧ Filter.Tendsto a Filter.atTop (nhds (sSup E)); constructorh.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ ∀ (n : ℕ), a n ∈ Eh.rightE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto a Filter.atTop (nhds (sSup E)); swaph.rightE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto a Filter.atTop (nhds (sSup E))h.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ ∀ (n : ℕ), a n ∈ E
  apply Filter.Tendsto.squeeze (g := fun n:ℕ ↦ sSup E - 1/(n+1:ℝ)) (h := fun _:ℕ ↦ sSup E)h.right.hgE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto (fun n ↦ sSup E - 1 / (↑n + 1)) Filter.atTop (nhds (sSup E))h.right.hhE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto (fun x ↦ sSup E) Filter.atTop (nhds (sSup E))h.right.hgfE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ (fun n ↦ sSup E - 1 / (↑n + 1)) ≤ ah.right.hfhE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ a ≤ fun x ↦ sSup Eh.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ ∀ (n : ℕ), a n ∈ E
  .h.right.hgE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto (fun n ↦ sSup E - 1 / (↑n + 1)) Filter.atTop (nhds (sSup E)) convert tendsto_const_nhds.sub (a := sSup E) (b := 0) _h.e'_1.h.e'_3E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ sSup E = sSup E - 0h.right.hg.convert_4E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto (fun n ↦ 1 / (↑n + 1)) Filter.atTop (nhds 0); simph.right.hg.convert_4E:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto (fun n ↦ 1 / (↑n + 1)) Filter.atTop (nhds 0)
    exact tendsto_one_div_add_atTop_nhds_zero_natAll goals completed! 🐙
  .h.right.hhE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X n⊢ Filter.Tendsto (fun x ↦ sSup E) Filter.atTop (nhds (sSup E)) exact tendsto_const_nhdsAll goals completed! 🐙
  all_goals intro _h.leftE:Set ℝhnon:E.Nonemptyhbound:BddAbove Ehclosed:IsClosed EX:ℕ → Set ℝ := fun n ↦ {x | x ∈ E ∧ sSup E - 1 / (↑n + 1) ≤ x ∧ x ≤ sSup E}hX:∀ (n : ℕ), Nonempty ↑(X n)a:ℕ → ℝ := fun n ↦ sInf (X n)ha:∀ (n : ℕ), a n ∈ X nn✝:ℕ⊢ a n✝ ∈ E; simp_all [X]All goals completed! 🐙

Proposition 8.4.7 / Exercise 8.4.1

theorem declaration uses `sorry`exists_function {X Y : Type} {P : X → Y → Prop} (h: ∀ x, ∃ y, P x y) :
  ∃ f : X → Y, ∀ x, P x (f x) := byX:TypeY:TypeP:X → Y → Proph:∀ (x : X), ∃ y, P x y⊢ ∃ f, ∀ (x : X), P x (f x)
  sorryAll goals completed! 🐙

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 declaration uses `sorry`axiom_of_choice_from_exists_function {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) :
  Nonempty (∀ i, X i) := byI:TypeX:I → Typeh:∀ (i : I), Nonempty (X i)⊢ Nonempty ((i : I) → X i)
  sorryAll goals completed! 🐙

Exercise 8.4.2

theorem declaration uses `sorry`exists_set_singleton_intersect {I U:Type} {X: I → Set U} (h: Set.PairwiseDisjoint .univ X)
  (hnon: ∀ α, Nonempty (X α)) :
  ∃ Y : Set U, ∀ α, Nat.card (Y ∩ X α : Set U) = 1 := byI:TypeU:TypeX:I → Set Uh:Set.univ.PairwiseDisjoint Xhnon:∀ (α : I), Nonempty ↑(X α)⊢ ∃ Y, ∀ (α : I), Nat.card ↑(Y ∩ X α) = 1
  sorryAll goals completed! 🐙

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 declaration uses `sorry`axiom_of_choice_from_exists_set_singleton_intersect {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) :
  Nonempty (∀ i, X i) := byI:TypeX:I → Typeh:∀ (i : I), Nonempty (X i)⊢ Nonempty ((i : I) → X i)
  sorryAll goals completed! 🐙

Exercise 8.4.3

theorem declaration uses `sorry`Function.Injective.inv_surjective {A B:Type} {g: B → A} (hg: Function.Surjective g) :
  ∃ f : A → B, Function.Injective f ∧ Function.RightInverse f g := byA:TypeB:Typeg:B → Ahg:Function.Surjective g⊢ ∃ f, Function.Injective f ∧ Function.RightInverse f g
  sorryAll goals completed! 🐙

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.

theorem declaration uses `sorry`axiom_of_choice_from_function_injective_inv_surjective {I: Type} {X: I → Type} (h : ∀ i, Nonempty (X i)) :
  Nonempty (∀ i, X i) := byI:TypeX:I → Typeh:∀ (i : I), Nonempty (X i)⊢ Nonempty ((i : I) → X i)
  sorryAll goals completed! 🐙

end Chapter8