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)
theorem
zorn.chain.total_of_refl
{α : Type u}
{r : α → α → Prop}
[is_refl α r]
{c : set α}
(H : zorn.chain r c)
{x y : α} :
theorem
zorn.chain.mono
{α : Type u}
{r : α → α → Prop}
{c c' : set α} :
c' ⊆ c → zorn.chain r c → zorn.chain r c'
theorem
zorn.chain.directed_on
{α : Type u}
{r : α → α → Prop}
[is_refl α r]
{c : set α} :
zorn.chain r c → directed_on r c
theorem
zorn.chain_insert
{α : Type u}
{r : α → α → Prop}
{c : set α}
{a : α} :
zorn.chain r c → (∀ (b : α), b ∈ c → b ≠ a → r a b ∨ r b a) → zorn.chain r (has_insert.insert a c)
super_chain c₁ c₂ means that c₂ is a chain that strictly includesc₁`.
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)
theorem
zorn.succ_spec
{α : Type u}
{r : α → α → Prop}
{c : set α} :
(∃ (c' : set α), zorn.chain r c ∧ zorn.super_chain c c') → zorn.super_chain c (zorn.succ_chain c)
theorem
zorn.chain_succ
{α : Type u}
{r : α → α → Prop}
{c : set α} :
zorn.chain r c → zorn.chain r (zorn.succ_chain c)
theorem
zorn.super_of_not_max
{α : Type u}
{r : α → α → Prop}
{c : set α} :
zorn.chain r c → ¬zorn.is_max_chain c → zorn.super_chain c (zorn.succ_chain 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 ⋃₀.
theorem
zorn.chain_closure_total
{α : Type u}
{r : α → α → Prop}
{c₁ c₂ : set α} :
zorn.chain_closure c₁ → zorn.chain_closure c₂ → c₁ ⊆ c₂ ∨ c₂ ⊆ c₁
theorem
zorn.chain_closure_succ_fixpoint
{α : Type u}
{r : α → α → Prop}
{c₁ c₂ : set α} :
zorn.chain_closure c₁ → zorn.chain_closure c₂ → zorn.succ_chain c₂ = c₂ → c₁ ⊆ c₂
theorem
zorn.chain_closure_succ_fixpoint_iff
{α : Type u}
{r : α → α → Prop}
{c : set α} :
zorn.chain_closure c → (zorn.succ_chain c = c ↔ c = ⋃₀zorn.chain_closure)
theorem
zorn.chain_chain_closure
{α : Type u}
{r : α → α → Prop}
{c : set α} :
zorn.chain_closure c → zorn.chain r c
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.
theorem
zorn.exists_maximal_of_chains_bounded
{α : Type u}
{r : α → α → Prop} :
(∀ (c : set α), zorn.chain r c → (∃ (ub : α), ∀ (a : α), a ∈ c → r a ub)) → (∀ {a b c : α}, r a b → r b c → r a c) → (∃ (m : α), ∀ (a : α), r m a → r a m)
Zorn's lemma
If every chain has an upper bound, then there is a maximal element
theorem
zorn.chain.image
{α : Type u_1}
{β : Type u_2}
(r : α → α → Prop)
(s : β → β → Prop)
(f : α → β)
(h : ∀ (x y : α), r x y → s (f x) (f y))
{c : set α} :
zorn.chain r c → zorn.chain s (f '' c)
theorem
directed_of_chain
{α : Type u_1}
{β : Type u_2}
{r : β → β → Prop}
[is_refl β r]
{f : α → β}
{c : set α} :
zorn.chain (f ⁻¹'o r) c → directed r (λ (x : {a // a ∈ c}), f ↑x)