doc-next-gen

Mathlib.Order.CompleteLattice.Chain

Module docstring

{"# 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. "}

ChainClosure inductive
(r : α → α → Prop) : Set α → Prop
Full source 
/-- Predicate for whether a set is reachable from `∅` using `SuccChain` and `⋃₀`. -/
inductive ChainClosure (r : α → α → Prop) : Set α → Prop
  | succ : ∀ {s}, ChainClosure r s → ChainClosure r (SuccChain r s)
  | union : ∀ {s}, (∀ a ∈ s, ChainClosure r a) → ChainClosure r (⋃₀s)
Chain closure under relation `r`
Informal description
The inductive predicate `ChainClosure r` defines for a relation `r` on a type `α` the sets that are reachable from the empty set by either applying the successor operation `SuccChain` or taking arbitrary unions (`⋃₀`). More precisely, a set `S` satisfies `ChainClosure r` if: 1. `S` is the empty set, or 2. `S` is obtained by applying `SuccChain` to some set `T` that already satisfies `ChainClosure r`, or 3. `S` is the union of a collection of sets that all satisfy `ChainClosure r`. This predicate is used in the proof of Hausdorff's maximality principle to construct maximal chains.
maxChain definition
(r : α → α → Prop) : Set α
Full source 
/-- An explicit maximal chain. `maxChain` is taken to be the union of all sets in `ChainClosure`. -/
def maxChain (r : α → α → Prop) : Set α := ⋃₀ setOf (ChainClosure r)
Maximal chain under relation \( r \) (Hausdorff's maximality principle)
Informal description
Given a relation \( r \) on a type \( \alpha \), the maximal chain \( \text{maxChain}(r) \) is defined as the union of all sets in the chain closure of \( r \), i.e., \( \text{maxChain}(r) = \bigcup₀ \{ S \mid \text{ChainClosure}(r, S) \} \).
chainClosure_maxChain theorem
: ChainClosure r (maxChain r)
Full source 
lemma chainClosure_maxChain : ChainClosure r (maxChain r) :=
  ChainClosure.union fun _ => id
Maximal Chain Satisfies Chain Closure Property
Informal description
The maximal chain $\text{maxChain}(r)$ under a relation $r$ on a type $\alpha$ satisfies the chain closure property $\text{ChainClosure}(r, \text{maxChain}(r))$.
ChainClosure.total theorem
(hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) : c₁ ⊆ c₂ ∨ c₂ ⊆ c₁
Full source 
lemma ChainClosure.total (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) :
    c₁ ⊆ c₂c₁ ⊆ c₂ ∨ c₂ ⊆ c₁ :=
  ((chainClosure_succ_total_aux hc₂) fun _ hc₃ => chainClosure_succ_total hc₃ hc₁).imp_left
    subset_succChain.trans
Total Ordering of Chain Closure Sets
Informal description
For any relation $r$ on a type $\alpha$ and any two sets $c_1, c_2 \subseteq \alpha$ in the chain closure of $r$, either $c_1$ is a subset of $c_2$ or $c_2$ is a subset of $c_1$.
ChainClosure.succ_fixpoint theorem
(hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂) (hc : SuccChain r c₂ = c₂) : c₁ ⊆ c₂
Full source 
lemma ChainClosure.succ_fixpoint (hc₁ : ChainClosure r c₁) (hc₂ : ChainClosure r c₂)
    (hc : SuccChain r c₂ = c₂) : c₁ ⊆ c₂ := by
  induction hc₁ with
  | succ hc₁ h => exact (chainClosure_succ_total hc₁ hc₂ h).elim (fun h => h ▸ hc.subset) id
  | union _ ih => exact sUnion_subset ih
Fixed Point of Successor Chain Operation is Maximal in Chain Closure
Informal description
Let $r$ be a relation on a type $\alpha$, and let $c_1, c_2 \subseteq \alpha$ be sets such that: 1. Both $c_1$ and $c_2$ are in the chain closure of $r$ (i.e., $c_1, c_2 \in \text{ChainClosure}(r)$), 2. $c_2$ is a fixed point of the successor chain operation (i.e., $\text{SuccChain}(r, c_2) = c_2$). Then $c_1$ is a subset of $c_2$ (i.e., $c_1 \subseteq c_2$).
ChainClosure.succ_fixpoint_iff theorem
(hc : ChainClosure r c) : SuccChain r c = c ↔ c = maxChain r
Full source 
lemma ChainClosure.succ_fixpoint_iff (hc : ChainClosure r c) :
    SuccChainSuccChain r c = c ↔ c = maxChain r :=
  ⟨fun h => (subset_sUnion_of_mem hc).antisymm <| chainClosure_maxChain.succ_fixpoint hc h,
    fun h => subset_succChain.antisymm' <| (subset_sUnion_of_mem hc.succ).trans h.symm.subset⟩
Fixed Point Characterization of Maximal Chain in Chain Closure
Informal description
Let $r$ be a relation on a type $\alpha$, and let $c \subseteq \alpha$ be a set in the chain closure of $r$ (i.e., $c \in \text{ChainClosure}(r)$). Then the successor chain $\text{SuccChain}(r, c)$ equals $c$ if and only if $c$ is the maximal chain $\text{maxChain}(r)$.
ChainClosure.isChain theorem
(hc : ChainClosure r c) : IsChain r c
Full source 
lemma ChainClosure.isChain (hc : ChainClosure r c) : IsChain r c := by
  induction hc with
  | succ _ h => exact h.succ
  | union hs h =>
    exact fun c₁ ⟨t₁, ht₁, (hc₁ : c₁ ∈ t₁)⟩ c₂ ⟨t₂, ht₂, (hc₂ : c₂ ∈ t₂)⟩ hneq =>
      ((hs _ ht₁).total <| hs _ ht₂).elim (fun ht => h t₂ ht₂ (ht hc₁) hc₂ hneq) fun ht =>
        h t₁ ht₁ hc₁ (ht hc₂) hneq
Chain Closure Preserves Chain Property
Informal description
For any relation $r$ on a type $\alpha$ and any subset $c \subseteq \alpha$ in the chain closure of $r$, the set $c$ is a chain with respect to $r$. That is, for any two distinct elements $x, y \in c$, either $x \prec y$ or $y \prec x$ holds.
maxChain_spec theorem
: IsMaxChain r (maxChain r)
Full source 
/-- **Hausdorff's maximality principle**

There exists a maximal totally ordered set of `α`.
Note that we do not require `α` to be partially ordered by `r`. -/
theorem maxChain_spec : IsMaxChain r (maxChain r) :=
  by_contradiction fun h =>
    let ⟨_, H⟩ := chainClosure_maxChain.isChain.superChain_succChain h
    H.ne (chainClosure_maxChain.succ_fixpoint_iff.mpr rfl).symm
Hausdorff's Maximality Principle: Existence of a Maximal Chain for Any Relation
Informal description
For any relation $r$ on a type $\alpha$, the set $\text{maxChain}(r)$ is a maximal chain with respect to $r$. That is, $\text{maxChain}(r)$ is a chain (totally ordered subset) under $r$, and there is no strictly larger chain containing it.