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, LinearOrder, and WellFoundedLT, with some API.
• Strong induction.
• Zorn's lemma.

@[implicit_reducible]

def Chapter8.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

Equations

• Chapter8.PartialOrder.mk hrefl hantisymm htrans = { le := fun (x1 x2 : X) => x1 ≤ x2, le_refl := hrefl, le_trans := htrans, lt_iff_le_not_ge := ⋯, le_antisymm := hantisymm }

def Chapter8.IsTotal (X : Type) [PartialOrder X] : Prop

Equations

• Chapter8.IsTotal X = ∀ (x y : X), x ≤ y ∨ y ≤ x

@[implicit_reducible]

noncomputable def Chapter8.LinearOrder.mk {X : Type} [PartialOrder X] (htotal : IsTotal X) : LinearOrder X

Equations

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

@[implicit_reducible]

noncomputable def Chapter8.LinearOrder.subtype {X : Type} [LinearOrder X] (A : Set X) : LinearOrder ↑A

Equations

• Chapter8.LinearOrder.subtype A = Chapter8.LinearOrder.mk ⋯

theorem Chapter8.IsTotal.subtype {X : Type} [PartialOrder X] {A : Set X} (hA : IsTotal X) : IsTotal ↑A

theorem Chapter8.IsTotal.subset {X : Type} [PartialOrder X] {A B : Set X} (hA : IsTotal ↑A) (hAB : B ⊆ A) : IsTotal ↑B

@[reducible, inline]

abbrev Chapter8.X_8_5_4 : Set (Set ℕ)

Equations

• Chapter8.X_8_5_4 = {{1, 2}, {2}, {2, 3}, {2, 3, 4}, {5}}

theorem Chapter8.IsMax.iff {X : Type} [PartialOrder X] (x : X) : IsMax x ↔ ¬∃ (y : X), x < y

Definition 8.5.5 (Maximal and minimal elements). Here we use Mathlib's IsMax and IsMin.

theorem Chapter8.IsMin.iff {X : Type} [PartialOrder X] (x : X) : IsMin x ↔ ¬∃ (y : X), x > y

theorem Chapter8.WellFoundedLT.iff (X : Type) [LinearOrder X] : WellFoundedLT X ↔ ∀ (A : Set X), A.Nonempty → ∃ (x : ↑A), IsMin x

Definition 8.5.8. We use [LinearOrder X] [WellFoundedLT X] to describe well-ordered sets.

theorem Chapter8.WellFoundedLT.iff' {X : Type} [PartialOrder X] (h : IsTotal X) : WellFoundedLT X ↔ ∀ (A : Set X), A.Nonempty → ∃ (x : ↑A), IsMin x

theorem Chapter8.IsMax.ofFinite {X : Type} [LinearOrder X] [Finite X] [Nonempty X] : ∃ (x : X), IsMax x

Exercise 8.5.8

theorem Chapter8.IsMin.ofFinite {X : Type} [LinearOrder X] [Finite X] [Nonempty X] : ∃ (x : X), IsMin x

theorem Chapter8.WellFoundedLT.ofFinite {X : Type} [LinearOrder X] [Finite X] : WellFoundedLT X

Exercise 8.5.8

theorem Chapter8.WellFoundedLT.subset {X : Type} [PartialOrder X] {A B : Set X} (hA : IsTotal ↑A) [hwell : WellFoundedLT ↑A] (hAB : B ⊆ A) : WellFoundedLT ↑B

theorem Chapter8.WellFoundedLT.strong_induction {X : Type} [LinearOrder X] [WellFoundedLT X] {P : X → Prop} (h : ∀ (n : X), (∀ m < n, P m) → P n) (n : X) : P n

Proposition 8.5.10 / Exercise 8.5.10

@[reducible, inline]

abbrev Chapter8.IsUpperBound {X : Type} [PartialOrder X] (A : Set X) (x : X) : Prop

Definition 8.5.12 (Upper bounds and strict upper bounds)

Equations

• Chapter8.IsUpperBound A x = ∀ y ∈ A, y ≤ x

theorem Chapter8.IsUpperBound.iff {X : Type} [PartialOrder X] (A : Set X) (x : X) : IsUpperBound A x ↔ x ∈ upperBounds A

Connection with Mathlib's upperBounds

@[reducible, inline]

abbrev Chapter8.IsStrictUpperBound {X : Type} [PartialOrder X] (A : Set X) (x : X) : Prop

Equations

• Chapter8.IsStrictUpperBound A x = (Chapter8.IsUpperBound A x ∧ x ∉ A)

theorem Chapter8.IsStrictUpperBound.iff {X : Type} [PartialOrder X] (A : Set X) (x : X) : IsStrictUpperBound A x ↔ ∀ y ∈ A, y < x

theorem Chapter8.IsStrictUpperBound.iff' {X : Type} [PartialOrder X] (A : Set X) (x : X) : IsStrictUpperBound A x ↔ x ∈ upperBounds A \ A

theorem Chapter8.IsMin.iff_lowerbound {X : Type} [PartialOrder X] {Y : Set X} (hY : IsTotal ↑Y) (x₀ : X) : (∃ (hx₀ : x₀ ∈ Y), IsMin ⟨x₀, hx₀⟩) ↔ x₀ ∈ Y ∧ ∀ x ∈ Y, x₀ ≤ x

A convenient way to simplify the notion of having x₀ as a minimal element.

theorem Chapter8.IsMin.iff_lowerbound' {X : Type} [PartialOrder X] {Y : Set X} (hY : IsTotal ↑Y) : (∃ (x₀ : ↑Y), IsMin x₀) ↔ ∃ x₀ ∈ Y, ∀ x ∈ Y, x₀ ≤ x

theorem Chapter8.WellFoundedLT.partialOrder {X : Type} [PartialOrder X] (x₀ : X) : ∃ (Y : Set X), IsTotal ↑Y ∧ WellFoundedLT ↑Y ∧ (∃ (hx₀ : x₀ ∈ Y), IsMin ⟨x₀, hx₀⟩) ∧ ¬∃ (x : X), IsStrictUpperBound Y x

Lemma 8.5.14

theorem Chapter8.Zorns_lemma {X : Type} [PartialOrder X] [Nonempty X] (hchain : ∀ (Y : Set X), IsTotal ↑Y ∧ Y.Nonempty → ∃ (x : X), IsUpperBound Y x) : ∃ (x : X), IsMax x

Lemma 8.5.15 (Zorn's lemma) / Exercise 8.5.14

def Chapter8.empty_set_partial_order [h₀ : LE Empty] : Decidable (∃ (h : PartialOrder Empty), LE.le = LE.le)

Exercise 8.5.1

Equations

• Chapter8.empty_set_partial_order = sorry

def Chapter8.empty_set_linear_order [h₀ : LE Empty] : Decidable (∃ (h : LinearOrder Empty), LE.le = LE.le)

Equations

• Chapter8.empty_set_linear_order = sorry

def Chapter8.empty_set_well_order [h₀ : LT Empty] : Decidable (Nonempty (WellFoundedLT Empty))

Equations

• Chapter8.empty_set_well_order = sorry

def Chapter8.Ex_8_5_5_b : Decidable (∀ (X Y : Type) (h : LinearOrder Y) (f : X → Y), ∃ (h₀ : LinearOrder X), LE.le = fun (x y : X) => f x < f y ∨ x = y)

Equations

• Chapter8.Ex_8_5_5_b = sorry

@[reducible, inline]

abbrev Chapter8.OrderIdeals (X : Type) [PartialOrder X] : Set (Set X)

Exercise 8.5.6

Equations

• Chapter8.OrderIdeals X = Set.Iic '' Set.univ

def Chapter8.OrderIdeals.iso {X : Type} [PartialOrder X] : X ≃o ↑(OrderIdeals X)

Equations

• Chapter8.OrderIdeals.iso = { toFun := fun (x : X) => ⟨Set.Iic x, ⋯⟩, invFun := sorry, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def Chapter8.Lex' (α : Type) : Type

Exercise 8.5.12. Here we make a copy of Mathlib's Lex wrapper for lexicographical orderings. This wrapper is needed because products X × Y of ordered sets are given the default instance of the product partial order instead of the lexicographical one.

Equations

• Chapter8.Lex' α = α

@[implicit_reducible]

instance Chapter8.Lex'.partialOrder {X Y : Type} [PartialOrder X] [PartialOrder Y] : PartialOrder (Lex' (X × Y))

Equations

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

@[implicit_reducible]

instance Chapter8.Lex'.linearOrder {X Y : Type} [LinearOrder X] [LinearOrder Y] : LinearOrder (Lex' (X × Y))

Equations

• Chapter8.Lex'.linearOrder = sorry

instance Chapter8.Lex'.WellFoundedLT {X Y : Type} [LinearOrder X] [_root_.WellFoundedLT X] [LinearOrder Y] [_root_.WellFoundedLT Y] : _root_.WellFoundedLT (Lex' (X × Y))