mathlib documentation

order.zorn

Chains and Zorn's lemmas #

This file defines chains for an arbitrary relation and proves several formulations of Zorn's Lemma, along with Hausdorff's Maximality Principle.

Main declarations #

Variants #

The primary statement of Zorn's lemma is exists_maximal_of_chains_bounded. Then it is specialized to particular relations:

Lemma names carry modifiers:

How-to #

This file comes across as confusing to those who haven't yet used it, so here is a detailed walkthrough:

  1. Know what relation on which type/set you're looking for. See Variants above. You can discharge some conditions to Zorn's lemma directly using a _nonempty variant.
  2. Write down the definition of your type/set, put a suffices : ∃ m, ∀ a, m ≺ a → a ≺ m, { ... }, (or whatever you actually need) followed by a apply some_version_of_zorn.
  3. Fill in the details. This is where you start talking about chains.

A typical proof using Zorn could look like this

lemma zorny_lemma : zorny_statement :=
begin
  let s : set α := {x | whatever x},
  suffices :  x  s,  y  s, y  x  y = x, -- or with another operator
  { exact proof_post_zorn },
  apply zorn.zorn_subset, -- or another variant
  rintro c hcs hc,
  obtain rfl | hcnemp := c.eq_empty_or_nonempty, -- you might need to disjunct on c empty or not
  { exact edge_case_construction,
      proof_that_edge_case_construction_respects_whatever,
      proof_that_edge_case_construction_contains_all_stuff_in_c },
  exact construction,
    proof_that_construction_respects_whatever,
    proof_that_construction_contains_all_stuff_in_c⟩,
end

Notes #

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

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
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
theorem zorn.chain.mono {α : Type u} {r : α → α → Prop} {c c' : set α} :
c' czorn.chain r czorn.chain r c'
theorem zorn.chain.directed_on {α : Type u} {r : α → α → Prop} [is_refl α r] {c : set α} (H : zorn.chain r c) :
theorem zorn.chain_insert {α : Type u} {r : α → α → Prop} {c : set α} {a : α} (hc : zorn.chain r c) (ha : ∀ (b : α), b cb ar a b r b a) :
def zorn.super_chain {α : Type u} {r : α → α → Prop} (c₁ c₂ : set α) :
Prop

super_chain c₁ c₂ means that c₂ is a chain that strictly includes c₁.

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

Set of sets reachable from using succ_chain and ⋃₀.

theorem zorn.chain_closure_empty {α : Type u} {r : α → α → Prop} :
theorem zorn.chain_closure_closure {α : Type u} {r : α → α → Prop} :
theorem zorn.chain_closure_total {α : Type u} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : c₁ zorn.chain_closure) (hc₂ : c₂ zorn.chain_closure) :
c₁ c₂ c₂ c₁
theorem zorn.chain_closure_succ_fixpoint {α : Type u} {r : α → α → Prop} {c₁ c₂ : set α} (hc₁ : c₁ zorn.chain_closure) (hc₂ : c₂ zorn.chain_closure) (h_eq : zorn.succ_chain c₂ = c₂) :
c₁ c₂
theorem zorn.chain_closure_succ_fixpoint_iff {α : Type u} {r : α → α → Prop} {c : set α} (hc : c zorn.chain_closure) :
theorem zorn.chain_chain_closure {α : Type u} {r : α → α → Prop} {c : set α} (hc : c zorn.chain_closure) :
def zorn.max_chain {α : Type u} {r : α → α → Prop} :
set α

An explicit maximal chain. max_chain is taken to be the union of all sets in chain_closure.

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

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} (h : ∀ (c : set α), zorn.chain r c(∃ (ub : α), ∀ (a : α), a cr a ub)) (trans : ∀ {a b c : α}, r a br b cr a c) :
∃ (m : α), ∀ (a : α), r m ar a m

Zorn's lemma

If every chain has an upper bound, then there exists a maximal element.

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

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

theorem zorn.chain.symm {α : Type u} {s : set α} {q : α → α → Prop} (h : zorn.chain q s) :

This can be used to turn zorn.chain (≥) into zorn.chain (≤) and vice-versa.

theorem zorn.zorn_partial_order {α : Type u} [partial_order α] (h : ∀ (c : set α), zorn.chain has_le.le c(∃ (ub : α), ∀ (a : α), a ca ub)) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn.zorn_nonempty_partial_order {α : Type u} [partial_order α] [nonempty α] (h : ∀ (c : set α), zorn.chain has_le.le cc.nonempty(∃ (ub : α), ∀ (a : α), a ca ub)) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn.zorn_partial_order₀ {α : Type u} [partial_order α] (s : set α) (ih : ∀ (c : set α), c szorn.chain has_le.le c(∃ (ub : α) (H : ub s), ∀ (z : α), z cz ub)) :
∃ (m : α) (H : m s), ∀ (z : α), z sm zz = m
theorem zorn.zorn_nonempty_partial_order₀ {α : Type u} [partial_order α] (s : set α) (ih : ∀ (c : set α), c szorn.chain has_le.le c∀ (y : α), y c(∃ (ub : α) (H : ub s), ∀ (z : α), z cz ub)) (x : α) (hxs : x s) :
∃ (m : α) (H : m s), x m ∀ (z : α), z sm zz = m
theorem zorn.zorn_subset {α : Type u} (S : set (set α)) (h : ∀ (c : set (set α)), c Szorn.chain has_subset.subset c(∃ (ub : set α) (H : ub S), ∀ (s : set α), s cs ub)) :
∃ (m : set α) (H : m S), ∀ (a : set α), a Sm aa = m
theorem zorn.zorn_subset_nonempty {α : Type u} (S : set (set α)) (H : ∀ (c : set (set α)), c Szorn.chain has_subset.subset cc.nonempty(∃ (ub : set α) (H : ub S), ∀ (s : set α), s cs ub)) (x : set α) (hx : x S) :
∃ (m : set α) (H : m S), x m ∀ (a : set α), a Sm aa = m
theorem zorn.zorn_superset {α : Type u} (S : set (set α)) (h : ∀ (c : set (set α)), c Szorn.chain has_subset.subset c(∃ (lb : set α) (H : lb S), ∀ (s : set α), s clb s)) :
∃ (m : set α) (H : m S), ∀ (a : set α), a Sa ma = m
theorem zorn.zorn_superset_nonempty {α : Type u} (S : set (set α)) (H : ∀ (c : set (set α)), c Szorn.chain has_subset.subset cc.nonempty(∃ (lb : set α) (H : lb S), ∀ (s : set α), s clb s)) (x : set α) (hx : x S) :
∃ (m : set α) (H : m S), m x ∀ (a : set α), a Sa ma = m
theorem zorn.chain.total {α : Type u} [preorder α] {c : set α} (H : zorn.chain has_le.le c) {x y : α} :
x cy cx y y x
theorem zorn.chain.image {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) (f : α → β) (h : ∀ (x y : α), r x ys (f x) (f y)) {c : set α} (hrc : 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 α} (h : zorn.chain (f ⁻¹'o r) c) :
directed r (λ (x : {a // a c}), f x)