@[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

@[reducible]

def Chapter8.PNat.divOrder : PartialOrder ℕ+

Exercise 8.5.3: The divisibility ordering on PNat.

Equations

• Chapter8.PNat.divOrder = { le := fun (x y : ℕ+) => ∃ (n : ℕ+), y = n * x, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := Chapter8.PNat.divOrder._proof_1, le_antisymm := ⋯ }

theorem Chapter8.PNat.divOrder_exists : ∃ (h₀ : PartialOrder ℕ+), LE.le = fun (x y : ℕ+) => ∃ (n : ℕ+), y = n * x

theorem Chapter8.PNat.divOrder_not_linear : ¬∃ (h₀ : LinearOrder ℕ+), LE.le = fun (x y : ℕ+) => ∃ (n : ℕ+), y = n * x

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))

theorem Chapter8.inj_trichotomy {X Y : Type} (h : ¬∃ (f : X → Y), Function.Injective f) : ∃ (g : Y → X), Function.Injective g

Exercise 8.5.15

@[implicit_reducible]

instance Chapter8.PartialOrder.coarserOrder (X : Type) : PartialOrder (PartialOrder X)

Exercise 8.5.16: The set of partial orderings on X, ordered by "coarser than", is itself a partial order.

Equations

• Chapter8.PartialOrder.coarserOrder X = { le := fun (p1 p2 : PartialOrder X) => ∀ (x y : X), x ≤ y → x ≤ y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

@[reducible]

def Chapter8.PartialOrder.discrete (X : Type) : PartialOrder X

The discrete ordering (x ≤ y ↔ x = y) is the unique minimal element.

Equations

• Chapter8.PartialOrder.discrete X = { le := fun (x y : X) => x = y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem Chapter8.PartialOrder.discrete_isBot (X : Type) (p : PartialOrder X) : discrete X ≤ p

theorem Chapter8.PartialOrder.discrete_isMin (X : Type) : IsMin (discrete X)

theorem Chapter8.PartialOrder.discrete_unique_min (X : Type) (p : PartialOrder X) (h : IsMin p) : p = discrete X

theorem Chapter8.PartialOrder.isMax_iff_isTotal (X : Type) (p : PartialOrder X) : IsMax p ↔ IsTotal X

A partial ordering is maximal in the coarser order iff it is total.

theorem Chapter8.PartialOrder.extends_to_total (X : Type) (p : PartialOrder X) : ∃ (q : PartialOrder X), p ≤ q ∧ IsTotal X

Any partial ordering extends to a total ordering (by Zorn's lemma).

theorem Chapter8.exists_set_singleton_intersect' {I U : Type} {X : I → Set U} (h : Set.univ.PairwiseDisjoint X) (hne : ∀ (α : I), Nonempty ↑(X α)) : ∃ (Y : Set U), ∀ (α : I), Nat.card ↑(Y ∩ X α) = 1

Exercise 8.5.17: Use Zorn's lemma to reprove Exercise 8.4.2

theorem Chapter8.hausdorff_of_zorns_lemma {X : Type} [PartialOrder X] : ∃ (M : Set X), Maximal (fun (S : Set X) => IsTotal ↑S) M

Exercise 8.5.18

theorem Chapter8.zorns_lemma_of_hausdorff {X : Type} [PartialOrder X] [Nonempty X] (hhausdorff : ∃ (M : Set X), Maximal (fun (S : Set X) => IsTotal ↑S) M) (hchain : ∀ (Y : Set X), IsTotal ↑Y ∧ Y.Nonempty → ∃ (x : X), IsUpperBound Y x) : ∃ (x : X), IsMax x

structure Chapter8.WellOrderedSubset (X : Type) : Type

Exercise 8.5.19: A well-ordered subset of X: a subset with a linear order and well-foundedness.

• carrier : Set X
• ord : LinearOrder ↑self.carrier
• wf : WellFoundedLT ↑self.carrier

def Chapter8.WellOrderedSubset.IsInitialSegment {X : Type} (W W' : WellOrderedSubset X) : Prop

(W, ≤) is an initial segment of (W', ≤') if W ⊆ W', the orderings agree on W, and W = {y ∈ W' : y <' x} for some x ∈ W'.

Equations

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

theorem Chapter8.WellOrderedSubset.IsInitialSegment.subset {X : Type} {W W' : WellOrderedSubset X} (h : W.IsInitialSegment W') : W.carrier ⊂ W'.carrier

@[implicit_reducible]

instance Chapter8.WellOrderedSubset.instPartialOrder (X : Type) : PartialOrder (WellOrderedSubset X)

The ordering on well-ordered subsets: equal or initial segment.

Equations

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

def Chapter8.WellOrderedSubset.empty (X : Type) : WellOrderedSubset X

The empty well-ordered subset.

Equations

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

theorem Chapter8.WellOrderedSubset.empty_isMin (X : Type) : IsMin (empty X)

theorem Chapter8.WellOrderedSubset.isMax_iff_full (X : Type) (W : WellOrderedSubset X) : IsMax W ↔ W.carrier = Set.univ

The maximal elements are precisely the well-orderings of all of X.

theorem Chapter8.well_ordering_principle (X : Type) : ∃ (l : LinearOrder X), WellFoundedLT X

The well-ordering principle: every set has a well-ordering.

theorem Chapter8.axiom_of_choice_of_well_ordering (hwo : ∀ (T : Type), ∃ (l : LinearOrder T), WellFoundedLT T) {I : Type} {X : I → Type} (hne : ∀ (i : I), Nonempty (X i)) : Nonempty ((i : I) → X i)

Well-ordering principle implies axiom of choice. Well-order the disjoint union Σ i, X i, then pick the minimum of each fiber.

theorem Chapter8.maximal_disjoint_subcollection {X : Type} (Ω : Set (Set X)) (hne : ∅ ∉ Ω) : ∃ Ω' ⊆ Ω, Ω'.Pairwise Disjoint ∧ ∀ C ∈ Ω, ∃ A ∈ Ω', (C ∩ A).Nonempty

Exercise 8.5.20

theorem Chapter8.exists_set_singleton_intersect_of_maximal_disjoint (hmds : ∀ (X : Type) (Ω : Set (Set X)), ∅ ∉ Ω → ∃ Ω' ⊆ Ω, Ω'.Pairwise Disjoint ∧ ∀ C ∈ Ω, ∃ A ∈ Ω', (C ∩ A).Nonempty) {I U : Type} {X : I → Set U} (h : Set.univ.PairwiseDisjoint X) (hne : ∀ (α : I), Nonempty ↑(X α)) : ∃ (Y : Set U), ∀ (α : I), Nat.card ↑(Y ∩ X α) = 1

The maximal disjoint subcollection property implies Exercise 8.4.2, hence is equivalent to the axiom of choice.