A chain is a subset c
satisfying
x ≺ y ∨ x = y ∨ y ≺ x
for all x y ∈ c
.
Equations
- zorn.chain r c = c.pairwise_on (λ (x y : α), r x y ∨ r y x)
super_chain c₁ c₂
means that c₂ is a chain that strictly includes
c₁`.
Equations
- zorn.super_chain c₁ c₂ = (zorn.chain r c₂ ∧ c₁ ⊂ c₂)
A chain c
is a maximal chain if there does not exists a chain strictly including c
.
Equations
- zorn.is_max_chain c = (zorn.chain r c ∧ ¬∃ (c' : set α), zorn.super_chain c c')
Given a set c
, if there exists a chain c'
strictly including c
, then succ_chain c
is one of these chains. Otherwise it is c
.
Equations
- zorn.succ_chain c = dite (∃ (c' : set α), zorn.chain r c ∧ zorn.super_chain c c') (λ (h : ∃ (c' : set α), zorn.chain r c ∧ zorn.super_chain c c'), classical.some h) (λ (h : ¬∃ (c' : set α), zorn.chain r c ∧ zorn.super_chain c c'), c)
- succ : ∀ {α : Type u} {r : α → α → Prop} {s : set α}, zorn.chain_closure s → zorn.chain_closure (zorn.succ_chain s)
- union : ∀ {α : Type u} {r : α → α → Prop} {s : set (set α)}, (∀ (a : set α), a ∈ s → zorn.chain_closure a) → zorn.chain_closure (⋃₀s)
Set of sets reachable from ∅
using succ_chain
and ⋃₀
.
max_chain
is the union of all sets in the chain closure.
Equations
Hausdorff's maximality principle
There exists a maximal totally ordered subset of α
.
Note that we do not require α
to be partially ordered by r
.
Zorn's lemma
If every chain has an upper bound, then there is a maximal element
If every nonempty chain of a nonempty type has an upper bound, then there is a maximal element. (A variant of Zorn's lemma.)