/-- **The axiom of choice, as a proposition.** Every family `X i` (`i : ι`) of non-empty types hasa choice function `c` with `c i : X i` for every `i`. -/def ChoiceFunctions : Prop := ∀ (ι : Type u) (X : ι → Type u), (∀ i, Nonempty (X i)) → Nonempty (∀ i, X i)
/-- **Every surjection splits:** for every surjective `p : α → β` there is a map `s : β → α` with`p (s b) = b` for all `b` (a *section*, or right inverse, of `p`). -/def SurjectionsSplit : Prop := ∀ (α β : Type u) (p : α → β), Function.Surjective p → ∃ s : β → α, ∀ b, p (s b) = b
split_of_choicetheoremProved here from basic factsNo axioms
split_of_choiceLean 4Proved here from basic factsFormally verified
/-- **Choice ⇒ every surjection splits.** For each `b` the fibre `{a // p a = b}` is non-emptybecause `p` is surjective; a choice function on the family of fibres is a section of `p`. -/theorem split_of_choice : ChoiceFunctions.{u} → SurjectionsSplit.{u} := by intro hc α β p hp have hfib : ∀ b, Nonempty {a // p a = b} := fun b => let ⟨a, ha⟩ := hp b ⟨⟨a, ha⟩⟩ obtain ⟨c⟩ := hc β (fun b => {a // p a = b}) hfib exact ⟨fun b => (c b).1, fun b => (c b).2⟩
choice_of_splittheoremProved here from basic factsNo axioms
choice_of_splitLean 4Proved here from basic factsFormally verified
/-- **Every surjection splits ⇒ choice.** The projection from the disjoint union `Σ i, X i` onto`ι` is surjective, because every `X i` is non-empty. A section `s` picks for each `i` a point`s i` of the union lying over `i` — that is, an element of `X i`. -/theorem choice_of_split : SurjectionsSplit.{u} → ChoiceFunctions.{u} := by intro hs ι X hX have hp : Function.Surjective (Sigma.fst : (Σ i, X i) → ι) := fun i => let ⟨x⟩ := hX i ⟨⟨i, x⟩, rfl⟩ obtain ⟨s, hs'⟩ := hs (Σ i, X i) ι Sigma.fst hp -- `(s i).2 : X (s i).1`, and `(s i).1 = i`: transport along that equation. exact ⟨fun i => hs' i ▸ (s i).2⟩
choice_holdstheoremApplies a library theoremClassical.choice
choice_holdsLean 4Applies a library theoremFormally verified
/-- **In Lean, choice is a theorem**, because Lean's logic includes the axiom `Classical.choice`(from a proof that a type is non-empty, produce an element of it). -/theorem choice_holds : ChoiceFunctions.{u} := fun _ _ hX => ⟨fun i => Classical.choice (hX i)⟩
surj_invtheoremApplies a library theoremClassical.choice
surj_invLean 4Applies a library theoremFormally verified
/-- Mathlib's version of "every surjection splits": `Function.surjInv` is a right inverse of anysurjection (`Function.rightInverse_surjInv`); it is built with `Classical.choose`. -/theorem surj_inv {α : Type u} {β : Type v} {p : α → β} (hp : Function.Surjective p) : ∀ b, p (Function.surjInv hp b) = b := Function.rightInverse_surjInv hp
well_orderingtheoremApplies a library theorempropext, Classical.choice, Quot.sound
well_orderingLean 4Applies a library theoremFormally verified
/-- **The well-ordering theorem:** every type carries a well-order. Mathlib's `WellOrderingRel`pulls back the well-order of the cardinals along an injection chosen with `Classical.choice`. -/theorem well_ordering (α : Type u) : ∃ r : α → α → Prop, IsWellOrder α r := ⟨WellOrderingRel, WellOrderingRel.isWellOrder⟩
exists_maximal_idealtheoremProved here from basic factspropext, Classical.choice, Quot.sound
exists_maximal_idealLean 4Proved here from basic factsFormally verified
/-- **Every non-zero commutative ring has a maximal ideal**, by Zorn's lemma as in the lesson.Order the proper ideals by inclusion. A non-empty chain `c` has the upper bound `⋃ c` (in Lean,`sSup c`), which is proper: if `1 ∈ sSup c` then `1` lies in a single member of the chain,which would then be the whole ring. Zorn gives a maximal proper ideal. -/theorem exists_maximal_ideal (R : Type u) [CommRing R] [Nontrivial R] : ∃ M : Ideal R, M.IsMaximal := by let S : Set (Ideal R) := {I | I ≠ ⊤} have hbot : (⊥ : Ideal R) ∈ S := bot_ne_top have chains : ∀ c ⊆ S, IsChain (· ≤ ·) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub := by intro c hcS hc y hy refine ⟨sSup c, ?_, fun z hz => le_sSup hz⟩ intro htop have h1 : (1 : R) ∈ sSup c := by rw [htop]; exact Submodule.mem_top obtain ⟨I, hIc, h1I⟩ := (Submodule.mem_sSup_of_directed ⟨y, hy⟩ hc.directedOn).mp h1 exact hcS hIc ((Ideal.eq_top_iff_one I).mpr h1I) obtain ⟨M, -, hM⟩ := zorn_le_nonempty₀ S chains ⊥ hbot refine ⟨M, Ideal.isMaximal_def.mpr ⟨hM.prop, fun I hMI => ?_⟩⟩ by_contra hI exact hMI.ne (hM.eq_of_le hI hMI.le)
exists_maximal_ideal_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
exists_maximal_ideal_libraryLean 4Applies a library theoremFormally verified
/-- The same theorem from Mathlib: `Ideal.exists_maximal` (Krull's theorem), proved there withZorn's lemma as well. -/theorem exists_maximal_ideal_library (R : Type u) [CommRing R] [Nontrivial R] : ∃ M : Ideal R, M.IsMaximal := Ideal.exists_maximal R
exists_basistheoremApplies a library theorempropext, Classical.choice, Quot.sound
exists_basisLean 4Applies a library theoremFormally verified
/-- **Every vector space has a basis.** Mathlib's `Module.Basis.ofVectorSpace` extends the emptylinearly independent set to a maximal one using Zorn's lemma. This holds over any divisionring `K`, for spaces of any dimension. -/theorem exists_basis (K : Type u) (V : Type v) [DivisionRing K] [AddCommGroup V] [Module K V] : ∃ s : Set V, Nonempty (Module.Basis s K V) := ⟨Module.Basis.ofVectorSpaceIndex K V, ⟨Module.Basis.ofVectorSpace K V⟩⟩
diaconescutheoremProved here from basic factspropext, Quot.sound
diaconescuLean 4Proved here from basic factsFormally verified
/-- **Diaconescu's theorem.** Suppose `ε` chooses, from every non-empty collection `P` ofpropositions, a member `ε P` of it. Then every proposition `p` is true or false.Let `U = {x | x = True ∨ p}` and `V = {x | x = False ∨ p}`, both non-empty.* If `ε U = True` and `ε V = False`, then `p` is false: if `p` held, `U` and `V` would be the same collection (extensionality: `funext`, `propext`), so `ε U = ε V`, i.e. `True = False`.* Otherwise one of the choices came from the `∨ p` half, and `p` is true.No excluded middle is used anywhere in the proof. -/theorem diaconescu (ε : (Prop → Prop) → Prop) (hε : ∀ P : Prop → Prop, (∃ x, P x) → P (ε P)) (p : Prop) : p ∨ ¬p := by let U : Prop → Prop := fun x => x = True ∨ p let V : Prop → Prop := fun x => x = False ∨ p have hU : U (ε U) := hε U ⟨True, Or.inl rfl⟩ have hV : V (ε V) := hε V ⟨False, Or.inl rfl⟩ -- If `p` holds, `U` and `V` are the same collection, so `ε` picks the same member. have same : p → ε U = ε V := fun hp => congrArg ε (funext fun x => propext ⟨fun _ => Or.inr hp, fun _ => Or.inr hp⟩) rcases hU with hu | hp · rcases hV with hv | hp · right intro hp have htf : True = False := by have h := same hp rw [hu, hv] at h exact h exact Eq.mp htf True.intro · exact Or.inl hp · exact Or.inl hp
em_librarytheoremApplies a library theorempropext, Classical.choice, Quot.sound
em_libraryLean 4Applies a library theoremFormally verified
/-- Core Lean's **law of excluded middle**, `Classical.em`, is not an axiom: it is proved from`Classical.choice`, `propext` and `funext` by Diaconescu's argument. -/theorem em_library (p : Prop) : p ∨ ¬p := Classical.em p
/-- Choice implies that every surjection has a section.Hint: apply the choice principle `hc` to the family of fibres `fun b => {a // p a = b}`. -/theorem split_of_choice : ChoiceFunctions.{u} → SurjectionsSplit.{u} := by sorry
Show the compiled solution
split_of_choiceLean 4Proved here from basic factsFormally verified
/-- **Choice ⇒ every surjection splits.** For each `b` the fibre `{a // p a = b}` is non-emptybecause `p` is surjective; a choice function on the family of fibres is a section of `p`. -/theorem split_of_choice : ChoiceFunctions.{u} → SurjectionsSplit.{u} := by intro hc α β p hp have hfib : ∀ b, Nonempty {a // p a = b} := fun b => let ⟨a, ha⟩ := hp b ⟨⟨a, ha⟩⟩ obtain ⟨c⟩ := hc β (fun b => {a // p a = b}) hfib exact ⟨fun b => (c b).1, fun b => (c b).2⟩
/-- If every surjection has a section, then choice holds.Hint: the projection `Sigma.fst : (Σ i, X i) → ι` is surjective. If `s` is a section, then`(s i).2 : X (s i).1`, and you can transport it along `(s i).1 = i` with `▸`. -/theorem choice_of_split : SurjectionsSplit.{u} → ChoiceFunctions.{u} := by sorry
Show the compiled solution
choice_of_splitLean 4Proved here from basic factsFormally verified
/-- **Every surjection splits ⇒ choice.** The projection from the disjoint union `Σ i, X i` onto`ι` is surjective, because every `X i` is non-empty. A section `s` picks for each `i` a point`s i` of the union lying over `i` — that is, an element of `X i`. -/theorem choice_of_split : SurjectionsSplit.{u} → ChoiceFunctions.{u} := by intro hs ι X hX have hp : Function.Surjective (Sigma.fst : (Σ i, X i) → ι) := fun i => let ⟨x⟩ := hX i ⟨⟨i, x⟩, rfl⟩ obtain ⟨s, hs'⟩ := hs (Σ i, X i) ι Sigma.fst hp -- `(s i).2 : X (s i).1`, and `(s i).1 = i`: transport along that equation. exact ⟨fun i => hs' i ▸ (s i).2⟩