Analysis I, Section 8.5: Ordered sets

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 PartialOrder.{u_2} (α : Type u_2) : Type u_2PartialOrder, LinearOrder.{u_2} (α : Type u_2) : Type u_2LinearOrder, and WellFoundedLT.{u_1} (α : Type u_1) [LT α] : PropWellFoundedLT, with some API.

• Strong induction.

• Zorn's lemma.

namespace Chapter8 example {X:Type} [PartialOrder X] {x y:X} (h₁: x ≤ y) (h₂: y ≤ x) : x = y := antisymm h₁ h₂example {X:Type} [PartialOrder X] {x y z:X} (h₁: x ≤ y) (h₂: y ≤ z) : x ≤ z := le_trans h₁ h₂example {X:Type} [PartialOrder X] (x y:X) : x < y ↔ x ≤ y ∧ x ≠ y := lt_iff_le_and_nedef PartialOrder.mk {X:Type} [LE X] (hrefl: ∀ x:X, x ≤ x) (hantisymm: ∀ x y:X, x ≤ y → y ≤ x → x = y) (htrans: ∀ x y z:X, x ≤ y → y ≤ z → x ≤ z) : PartialOrder X := { le := (·≤ ·) le_refl := hrefl le_antisymm := hantisymm le_trans := htrans }example {X:Type} : PartialOrder (Set X) := byX:Type⊢ PartialOrder (Set X) infer_instanceAll goals completed! 🐙example {X:Type} (A B: Set X) : A ≤ B ↔ A ⊆ B := byX:TypeA:Set XB:Set X⊢ A ≤ B ↔ A ⊆ B rflAll goals completed! 🐙 def IsTotal (X:Type) [PartialOrder X] : Prop := ∀ x y:X, x ≤ y ∨ y ≤ xexample {X:Type} [LinearOrder X] : IsTotal X := le_totalopen Classical in noncomputable def LinearOrder.mk {X:Type} [PartialOrder X] (htotal: IsTotal X) : LinearOrder X := { le_total := htotal toDecidableLE := decRel LE.le }

inferInstanceAs (LinearOrder ℕ) : LinearOrder ℕ

inferInstanceAs (LinearOrder ℚ) : LinearOrder ℚ

inferInstanceAs (LinearOrder ℝ) : LinearOrder ℝ

inferInstanceAs (LinearOrder EReal) : LinearOrder EReal

noncomputable def declaration uses 'sorry'LinearOrder.subtype {X:Type} [LinearOrder X] (A: Set X) : LinearOrder A := LinearOrder.mk (byX:Typeinst✝:LinearOrder XA:Set X⊢ IsTotal ↑A sorryAll goals completed! 🐙 )theorem IsTotal.subtype {X:Type} [PartialOrder X] {A: Set X} (hA: IsTotal X) : IsTotal A := byX:Typeinst✝:PartialOrder XA:Set XhA:IsTotal X⊢ IsTotal ↑A intro ⟨ x, hx ⟩ ⟨ y, hy ⟩X:Typeinst✝:PartialOrder XA:Set XhA:IsTotal Xx:Xhx:x ∈ Ay:Xhy:y ∈ A⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩ ∨ ⟨y, hy⟩ ≤ ⟨x, hx⟩ specialize hA x yX:Typeinst✝:PartialOrder XA:Set Xx:Xhx:x ∈ Ay:Xhy:y ∈ AhA:x ≤ y ∨ y ≤ x⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩ ∨ ⟨y, hy⟩ ≤ ⟨x, hx⟩; simp_allAll goals completed! 🐙theorem IsTotal.subset {X:Type} [PartialOrder X] {A B: Set X} (hA: IsTotal A) (hAB: B ⊆ A) : IsTotal B := byX:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ A⊢ IsTotal ↑B intro ⟨ x, hx ⟩ ⟨ y, hy ⟩X:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ Ax:Xhx:x ∈ By:Xhy:y ∈ B⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩ ∨ ⟨y, hy⟩ ≤ ⟨x, hx⟩ specialize hA ⟨ x, hAB hx ⟩ ⟨ y, hAB hy ⟩X:Typeinst✝:PartialOrder XA:Set XB:Set XhAB:B ⊆ Ax:Xhx:x ∈ By:Xhy:y ∈ BhA:⟨x, ⋯⟩ ≤ ⟨y, ⋯⟩ ∨ ⟨y, ⋯⟩ ≤ ⟨x, ⋯⟩⊢ ⟨x, hx⟩ ≤ ⟨y, hy⟩ ∨ ⟨y, hy⟩ ≤ ⟨x, hx⟩; simp_allAll goals completed! 🐙abbrev X_8_5_4 : Set (Set ℕ) := { {1,2}, {2}, {2,3}, {2,3,4}, {5} }declaration uses 'sorry'example : ¬ IsTotal X_8_5_4 := by⊢ ¬IsTotal ↑X_8_5_4 sorryAll goals completed! 🐙 theorem IsMin.iff {X:Type} [PartialOrder X] (x:X) : IsMin x ↔ ¬ ∃ y, x > y := byX:Typeinst✝:PartialOrder Xx:X⊢ IsMin x ↔ ¬∃ y, x > y rw [isMin_iff_forall_not_lt]X:Typeinst✝:PartialOrder Xx:X⊢ (∀ (b : X), ¬b < x) ↔ ¬∃ y, x > y; grindAll goals completed! 🐙 declaration uses 'sorry'example : IsMax (⟨ {1,2}, by⊢ {1, 2} ∈ X_8_5_4 aesopAll goals completed! 🐙 ⟩ : X_8_5_4) := by⊢ IsMax ⟨{1, 2}, ⋯⟩ sorryAll goals completed! 🐙declaration uses 'sorry'example : IsMax (⟨ {2,3,4}, by⊢ {2, 3, 4} ∈ X_8_5_4 aesopAll goals completed! 🐙 ⟩ : X_8_5_4) := by⊢ IsMax ⟨{2, 3, 4}, ⋯⟩ sorryAll goals completed! 🐙declaration uses 'sorry'example : IsMin (⟨ {5}, by⊢ {5} ∈ X_8_5_4 aesopAll goals completed! 🐙 ⟩ : X_8_5_4) ∧ IsMax (⟨ {5}, by⊢ {5} ∈ X_8_5_4 aesopAll goals completed! 🐙 ⟩ : X_8_5_4) := by⊢ IsMin ⟨{5}, ⋯⟩ ∧ IsMax ⟨{5}, ⋯⟩ sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ IsMin (⟨ {2,3}, by⊢ {2, 3} ∈ X_8_5_4 aesopAll goals completed! 🐙 ⟩ : X_8_5_4) ∧ ¬ IsMax (⟨ {2,3}, by⊢ {2, 3} ∈ X_8_5_4 aesopAll goals completed! 🐙 ⟩ : X_8_5_4) := by⊢ ¬IsMin ⟨{2, 3}, ⋯⟩ ∧ ¬IsMax ⟨{2, 3}, ⋯⟩ sorryAll goals completed! 🐙 declaration uses 'sorry'example (n:ℕ) : ¬ IsMax n := byn:ℕ⊢ ¬IsMax n sorryAll goals completed! 🐙declaration uses 'sorry'example (n:ℤ): ¬ IsMin n ∧ ¬ IsMax n := byn:ℤ⊢ ¬IsMin n ∧ ¬IsMax n sorryAll goals completed! 🐙 theorem WellFoundedLT.iff' {X:Type} [PartialOrder X] (h: IsTotal X) : WellFoundedLT X ↔ ∀ A:Set X, A.Nonempty → ∃ x:A, IsMin x := @iff X (LinearOrder.mk h) declaration uses 'sorry'example : ¬ WellFoundedLT ℚ := by⊢ ¬WellFoundedLT ℚ sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ WellFoundedLT ℝ := by⊢ ¬WellFoundedLT ℝ sorryAll goals completed! 🐙 theorem declaration uses 'sorry'IsMin.ofFinite {X:Type} [LinearOrder X] [Finite X] [Nonempty X] : ∃ x:X, IsMin x := byX:Typeinst✝²:LinearOrder Xinst✝¹:Finite Xinst✝:Nonempty X⊢ ∃ x, IsMin x sorryAll goals completed! 🐙 declaration uses 'sorry'example {X:Type} [LinearOrder X] [WellFoundedLT X] (A: Set X) : WellFoundedLT A := byX:Typeinst✝¹:LinearOrder Xinst✝:WellFoundedLT XA:Set X⊢ WellFoundedLT ↑A sorryAll goals completed! 🐙theorem WellFoundedLT.subset {X:Type} [PartialOrder X] {A B: Set X} (hA: IsTotal A) [hwell: WellFoundedLT A] (hAB: B ⊆ A) : WellFoundedLT B := byX:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑Ahwell:WellFoundedLT ↑AhAB:B ⊆ A⊢ WellFoundedLT ↑B set hAlin : LinearOrder A := LinearOrder.mk hAX:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑Ahwell:WellFoundedLT ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124⊢ WellFoundedLT ↑B set hBlin : LinearOrder B := LinearOrder.mk (hA.subset hAB)X:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑Ahwell:WellFoundedLT ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯⊢ WellFoundedLT ↑B rw [iff] at hwell ⊢X:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hwell:∀ (A_1 : Set ↑A), A_1.Nonempty → ∃ x, IsMin xhBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯⊢ ∀ (A : Set ↑B), A.Nonempty → ∃ x, IsMin x; intro C hCX:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hwell:∀ (A_1 : Set ↑A), A_1.Nonempty → ∃ x, IsMin xhBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯C:Set ↑BhC:C.Nonempty⊢ ∃ x, IsMin x have ⟨ ⟨ ⟨ x, hx ⟩, hx' ⟩, hmin ⟩ := hwell ((B.embeddingOfSubset _ hAB) '' C) (byX:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hwell:∀ (A_1 : Set ↑A), A_1.Nonempty → ∃ x, IsMin xhBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯C:Set ↑BhC:C.Nonempty⊢ (⇑(B.embeddingOfSubset A hAB) '' C).Nonempty aesopAll goals completed! 🐙) simp at hx'X:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hwell:∀ (A_1 : Set ↑A), A_1.Nonempty → ∃ x, IsMin xhBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯C:Set ↑BhC:C.Nonemptyx:Xhx:x ∈ Ahx'✝:⟨x, hx⟩ ∈ ⇑(B.embeddingOfSubset A hAB) '' Chmin:IsMin ⟨⟨x, hx⟩, hx'✝⟩hx':∃ a, ∃ (b : a ∈ B), ⟨a, b⟩ ∈ C ∧ (B.embeddingOfSubset A hAB) ⟨a, b⟩ = ⟨x, hx⟩⊢ ∃ x, IsMin x; choose y hy hyC this using hx'X:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hwell:∀ (A_1 : Set ↑A), A_1.Nonempty → ∃ x, IsMin xhBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯C:Set ↑BhC:C.Nonemptyx:Xhx:x ∈ Ahx':⟨x, hx⟩ ∈ ⇑(B.embeddingOfSubset A hAB) '' Chmin:IsMin ⟨⟨x, hx⟩, hx'⟩y:Xhy:y ∈ BhyC:⟨y, hy⟩ ∈ Cthis:(B.embeddingOfSubset A hAB) ⟨y, hy⟩ = ⟨x, hx⟩⊢ ∃ x, IsMin x; use ⟨ _, hyC ⟩hX:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hwell:∀ (A_1 : Set ↑A), A_1.Nonempty → ∃ x, IsMin xhBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯C:Set ↑BhC:C.Nonemptyx:Xhx:x ∈ Ahx':⟨x, hx⟩ ∈ ⇑(B.embeddingOfSubset A hAB) '' Chmin:IsMin ⟨⟨x, hx⟩, hx'⟩y:Xhy:y ∈ BhyC:⟨y, hy⟩ ∈ Cthis:(B.embeddingOfSubset A hAB) ⟨y, hy⟩ = ⟨x, hx⟩⊢ IsMin ⟨⟨y, hy⟩, hyC⟩ simp_all [IsMin, Set.embeddingOfSubset]hX:Typeinst✝:PartialOrder XA:Set XB:Set XhA:IsTotal ↑AhAB:B ⊆ AhAlin:LinearOrder ↑_fvar.63122 := Chapter8.LinearOrder.mk _fvar.63124hBlin:LinearOrder ↑_fvar.63123 := Chapter8.LinearOrder.mk ⋯C:Set ↑Bx:Xhx:x ∈ Ahx':⟨x, hx⟩ ∈ ⇑(B.embeddingOfSubset A hAB) '' Cy:Xhy:y ∈ BhyC:⟨y, hy⟩ ∈ Chwell:∀ (A_1 : Set ↑A), A_1.Nonempty → ∃ a, (∃ (x : a ∈ A), ⟨a, ⋯⟩ ∈ A_1) ∧ ∀ (a_1 : X) (b : a_1 ∈ A), ⟨a_1, b⟩ ∈ A_1 → a_1 ≤ a → a ≤ a_1hC:C.Nonemptyhmin:∀ a ∈ A, ∀ (x_1 : X) (x_2 : x_1 ∈ B), ⟨x_1, ⋯⟩ ∈ C → x_1 = a → a ≤ x → x ≤ athis:y = x⊢ ∀ (a : X) (b : a ∈ B), ⟨a, b⟩ ∈ C → a ≤ x → x ≤ a; grindAll goals completed! 🐙 abbrev IsStrictUpperBound {X:Type} [PartialOrder X] (A:Set X) (x:X) : Prop := IsUpperBound A x ∧ x ∉ Atheorem declaration uses 'sorry'IsStrictUpperBound.iff {X:Type} [PartialOrder X] (A:Set X) (x:X) : IsStrictUpperBound A x ↔ ∀ y ∈ A, y < x := byX:Typeinst✝:PartialOrder XA:Set Xx:X⊢ IsStrictUpperBound A x ↔ ∀ y ∈ A, y < x sorryAll goals completed! 🐙theorem IsStrictUpperBound.iff' {X:Type} [PartialOrder X] (A:Set X) (x:X) : IsStrictUpperBound A x ↔ x ∈ upperBounds A \ A := byX:Typeinst✝:PartialOrder XA:Set Xx:X⊢ IsStrictUpperBound A x ↔ x ∈ upperBounds A \ A simp [IsStrictUpperBound, IsUpperBound.iff]All goals completed! 🐙declaration uses 'sorry'example : IsUpperBound (.Icc 1 2: Set ℝ) 2 := by⊢ IsUpperBound (Set.Icc 1 2) 2 sorryAll goals completed! 🐙declaration uses 'sorry'example : ¬ IsStrictUpperBound (.Icc 1 2: Set ℝ) 2 := by⊢ ¬IsStrictUpperBound (Set.Icc 1 2) 2 sorryAll goals completed! 🐙declaration uses 'sorry'example : IsStrictUpperBound (.Icc 1 2: Set ℝ) 3 := by⊢ IsStrictUpperBound (Set.Icc 1 2) 3 sorryAll goals completed! 🐙 theorem IsMin.iff_lowerbound' {X:Type} [PartialOrder X] {Y: Set X} (hY: IsTotal Y) : (∃ x₀ : Y, IsMin x₀) ↔ ∃ x₀, x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x := byX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Y⊢ (∃ x₀, IsMin x₀) ↔ ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x constructormpX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Y⊢ (∃ x₀, IsMin x₀) → ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ xmprX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Y⊢ (∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x) → ∃ x₀, IsMin x₀ .mpX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Y⊢ (∃ x₀, IsMin x₀) → ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x intro ⟨ ⟨ x₀, hx₀ ⟩, hmin ⟩mpX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Yx₀:Xhx₀:x₀ ∈ Yhmin:IsMin ⟨x₀, hx₀⟩⊢ ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x have : ∃ (hx₀ : x₀ ∈ Y), IsMin (⟨ _, hx₀ ⟩:Y) := byX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Y⊢ (∃ x₀, IsMin x₀) ↔ ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x use hx₀All goals completed! 🐙 rw [iff_lowerbound hY x₀] at thismpX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Yx₀:Xhx₀:x₀ ∈ Yhmin:IsMin ⟨x₀, hx₀⟩this:x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x⊢ ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x; use x₀All goals completed! 🐙 intro ⟨ x₀, hx₀, hmin ⟩mprX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Yx₀:Xhx₀:x₀ ∈ Yhmin:∀ x ∈ Y, x₀ ≤ x⊢ ∃ x₀, IsMin x₀; choose hx₀ _ using (iff_lowerbound hY x₀).mpr ⟨ hx₀, hmin ⟩mprX:Typeinst✝:PartialOrder XY:Set XhY:IsTotal ↑Yx₀:Xhx₀✝:x₀ ∈ Yhmin:∀ x ∈ Y, x₀ ≤ xhx₀:x₀ ∈ Yx✝:IsMin ⟨x₀, hx₀⟩⊢ ∃ x₀, IsMin x₀; use ⟨ _, hx₀ ⟩All goals completed! 🐙