Hausdorff's maximality principle

This file proves Hausdorff's maximality principle.

Main declarations

• maxChain_spec: Hausdorff's Maximality Principle.

Notes

Originally ported from Isabelle/HOL. The original file was written by Jacques D. Fleuriot, Tobias Nipkow, Christian Sternagel.

inductive ChainClosure {α : Type u_1} (r : α → α → Prop) : Set α → Prop

Predicate for whether a set is reachable from ∅ using SuccChain and ⋃₀.

• succ {α : Type u_1} {r : α → α → Prop} {s : Set α} : ChainClosure r s → ChainClosure r (SuccChain r s)
• union {α : Type u_1} {r : α → α → Prop} {s : Set (Set α)} : (∀ a ∈ s, ChainClosure r a) → ChainClosure r (⋃₀ s)

def maxChain {α : Type u_1} (r : α → α → Prop) : Set α

An explicit maximal chain. maxChain is taken to be the union of all sets in ChainClosure.

Equations

• maxChain r = ⋃₀ Set.ofPred (ChainClosure r)

theorem chainClosure_empty {α : Type u_1} {r : α → α → Prop} : ChainClosure r ∅

theorem chainClosure_maxChain {α : Type u_1} {r : α → α → Prop} : ChainClosure r (maxChain r)

theorem ChainClosure.total {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : Set α} (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) : c₁ ⊆ c₂ ∨ c₂ ⊆ c₁

theorem ChainClosure.succ_fixpoint {α : Type u_1} {r : α → α → Prop} {c₁ c₂ : Set α} (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) (hc : SuccChain r c₂ = c₂) : c₁ ⊆ c₂

theorem ChainClosure.succ_fixpoint_iff {α : Type u_1} {r : α → α → Prop} {c : Set α} (hc : ChainClosure r c) : SuccChain r c = c ↔ c = maxChain r

theorem ChainClosure.isChain {α : Type u_1} {r : α → α → Prop} {c : Set α} (hc : ChainClosure r c) : IsChain r c

theorem maxChain_spec {α : Type u_1} {r : α → α → Prop} : IsMaxChain r (maxChain r)

Hausdorff's maximality principle

There exists a maximal totally ordered set of α. Note that we do not require α to be partially ordered by r.