mathlib documentation

order.zorn

source
def zorn.chain {α : Type u} (r : α → α → Prop) (c : set α) :
Prop

A chain is a subset c satisfying x ≺ y ∨ x = y ∨ y ≺ x for all x y ∈ c.

Equations
source
theorem zorn.chain.total_of_refl {α : Type u} {r : α → α → Prop} [is_refl α r] {c : set α} (H : zorn.chain r c) {x y : α} (hx : x ∈ c) (hy : y ∈ c) :
r x y ∨ r y x
source
theorem zorn.chain.mono {α : Type u} {r : α → α → Prop} {c c' : set α} :
c' ⊆ c → zorn.chain r c → zorn.chain r c'
source
theorem zorn.chain.directed_on {α : Type u} {r : α → α → Prop} [is_refl α r] {c : set α} (H : zorn.chain r c) :
directed_on r c
source
theorem zorn.chain_insert {α : Type u} {r : α → α → Prop} {c : set α} {a : α} (hc : zorn.chain r c) (ha : ∀ (b : α), b ∈ c → b ≠ a → r a b ∨ r b a) :
zorn.chain r (insert a c)
source
def zorn.super_chain {α : Type u} {r : α → α → Prop} (c₁ c₂ : set α) :
Prop

super_chain c₁ c₂ means that c₂ is a chain that strictly includesc₁`.

Equations
source
def zorn.is_max_chain {α : Type u} {r : α → α → Prop} (c : set α) :
Prop

A chain c is a maximal chain if there does not exists a chain strictly including c.

Equations
source
def zorn.succ_chain {α : Type u} {r : α → α → Prop} (c : set α) :
set α

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
source
theorem zorn.succ_spec {α : Type u} {r : α → α → Prop} {c : set α} (h : ∃ (c' : set α), zorn.chain r c ∧ zorn.super_chain c c') :
zorn.super_chain c (zorn.succ_chain c)
source
theorem zorn.chain_succ {α : Type u} {r : α → α → Prop} {c : set α} (hc : zorn.chain r c) :
zorn.chain r (zorn.succ_chain c)
source
theorem zorn.super_of_not_max {α : Type u} {r : α → α → Prop} {c : set α} (hc₁ : zorn.chain r c) (hc₂ : ¬zorn.is_max_chain c) :
zorn.super_chain c (zorn.succ_chain c)
source
theorem zorn.succ_increasing {α : Type u} {r : α → α → Prop} {c : set α} :
c ⊆ zorn.succ_chain c
source
inductive zorn.chain_closure {α : Type u} {r : α → α → Prop} :
set α → Prop

Set of sets reachable from ∅ using succ_chain and ⋃₀.

source
theorem zorn.chain_closure_empty {α : Type u} {r : α → α → Prop} :
zorn.chain_closure ∅
source
theorem zorn.chain_closure_closure {α : Type u} {r : α → α → Prop} :
zorn.chain_closure (⋃₀zorn.chain_closure)
source
theorem zorn.chain_closure_total {α : Type u} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : zorn.chain_closure c₁) (hc₂ : zorn.chain_closure c₂) :
c₁ ⊆ c₂ ∨ c₂ ⊆ c₁
source
theorem zorn.chain_closure_succ_fixpoint {α : Type u} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : zorn.chain_closure c₁) (hc₂ : zorn.chain_closure c₂) (h_eq : zorn.succ_chain c₂ = c₂) :
c₁ ⊆ c₂
source
theorem zorn.chain_closure_succ_fixpoint_iff {α : Type u} {r : α → α → Prop} {c : set α} (hc : zorn.chain_closure c) :
zorn.succ_chain c = c ↔ c = ⋃₀zorn.chain_closure
source
theorem zorn.chain_chain_closure {α : Type u} {r : α → α → Prop} {c : set α} (hc : zorn.chain_closure c) :
zorn.chain r c
source
def zorn.max_chain {α : Type u} {r : α → α → Prop} :
set α

max_chain is the union of all sets in the chain closure.

Equations
source
theorem zorn.max_chain_spec {α : Type u} {r : α → α → Prop} :
zorn.is_max_chain zorn.max_chain

Hausdorff's maximality principle

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

source
theorem zorn.exists_maximal_of_chains_bounded {α : Type u} {r : α → α → Prop} (h : ∀ (c : set α), zorn.chain r c → (∃ (ub : α), ∀ (a : α), a ∈ c → r a ub)) (trans : ∀ {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

source
theorem zorn.exists_maximal_of_nonempty_chains_bounded {α : Type u} {r : α → α → Prop} [nonempty α] (h : ∀ (c : set α), zorn.chain r c → c.nonempty → (∃ (ub : α), ∀ (a : α), a ∈ c → r a ub)) (trans : ∀ {a b c : α}, r a b → r b c → r a c) :
∃ (m : α), ∀ (a : α), r m a → r a m

If every nonempty chain of a nonempty type has an upper bound, then there is a maximal element. (A variant of Zorn's lemma.)

source
theorem zorn.zorn_partial_order {α : Type u} [partial_order α] (h : ∀ (c : set α), zorn.chain has_le.le c → (∃ (ub : α), ∀ (a : α), a ∈ c → a ≤ ub)) :
∃ (m : α), ∀ (a : α), m ≤ a → a = m
source
theorem zorn.zorn_nonempty_partial_order {α : Type u} [partial_order α] [nonempty α] (h : ∀ (c : set α), zorn.chain has_le.le c → c.nonempty → (∃ (ub : α), ∀ (a : α), a ∈ c → a ≤ ub)) :
∃ (m : α), ∀ (a : α), m ≤ a → a = m
source
theorem zorn.zorn_partial_order₀ {α : Type u} [partial_order α] (s : set α) (ih : ∀ (c : set α), c ⊆ s → zorn.chain has_le.le c → ∀ (y : α), y ∈ c → (∃ (ub : α) (H : ub ∈ s), ∀ (z : α), z ∈ c → z ≤ ub)) (x : α) (hxs : x ∈ s) :
∃ (m : α) (H : m ∈ s), x ≤ m ∧ ∀ (z : α), z ∈ s → m ≤ z → z = m
source
theorem zorn.zorn_subset {α : Type u} (S : set (set α)) (h : ∀ (c : set (set α)), c ⊆ S → zorn.chain has_subset.subset c → (∃ (ub : set α) (H : ub ∈ S), ∀ (s : set α), s ∈ c → s ⊆ ub)) :
∃ (m : set α) (H : m ∈ S), ∀ (a : set α), a ∈ S → m ⊆ a → a = m
source
theorem zorn.zorn_subset₀ {α : Type u} (S : set (set α)) (H : ∀ (c : set (set α)), c ⊆ S → zorn.chain has_subset.subset c → c.nonempty → (∃ (ub : set α) (H : ub ∈ S), ∀ (s : set α), s ∈ c → s ⊆ ub)) (x : set α) (hx : x ∈ S) :
∃ (m : set α) (H : m ∈ S), x ⊆ m ∧ ∀ (a : set α), a ∈ S → m ⊆ a → a = m
source
theorem zorn.chain.total {α : Type u} [preorder α] {c : set α} (H : zorn.chain has_le.le c) {x y : α} :
x ∈ c → y ∈ c → x ≤ y ∨ y ≤ x
source
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 α} (hrc : zorn.chain r c) :
zorn.chain s (f '' c)
source
theorem directed_of_chain {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [is_refl β r] {f : α → β} {c : set α} (h : zorn.chain (f ⁻¹'o r) c) :
directed r (λ (x : {a // a ∈ c}), f ↑x)