mathlib documentation

order.zorn

Zorn's lemmas #

This file proves several formulations of Zorn's Lemma.

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_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.

theorem exists_maximal_of_chains_bounded {α : Type u_1} {r : α → α → Prop} (h : ∀ (c : set α), is_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 exists_maximal_of_nonempty_chains_bounded {α : Type u_1} {r : α → α → Prop} [nonempty α] (h : ∀ (c : set α), is_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_partial_order {α : Type u_1} [partial_order α] (h : ∀ (c : set α), is_chain has_le.le c(∃ (ub : α), ∀ (a : α), a ca ub)) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn_nonempty_partial_order {α : Type u_1} [partial_order α] [nonempty α] (h : ∀ (c : set α), is_chain has_le.le cc.nonempty(∃ (ub : α), ∀ (a : α), a ca ub)) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn_partial_order₀ {α : Type u_1} [partial_order α] (s : set α) (ih : ∀ (c : set α), c sis_chain has_le.le c(∃ (ub : α) (H : ub s), ∀ (z : α), z cz ub)) :
∃ (m : α) (H : m s), ∀ (z : α), z sm zz = m
theorem zorn_nonempty_partial_order₀ {α : Type u_1} [partial_order α] (s : set α) (ih : ∀ (c : set α), c sis_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_subset {α : Type u_1} (S : set (set α)) (h : ∀ (c : set (set α)), c Sis_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_subset_nonempty {α : Type u_1} (S : set (set α)) (H : ∀ (c : set (set α)), c Sis_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_superset {α : Type u_1} (S : set (set α)) (h : ∀ (c : set (set α)), c Sis_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_superset_nonempty {α : Type u_1} (S : set (set α)) (H : ∀ (c : set (set α)), c Sis_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 is_chain.exists_max_chain {α : Type u_1} {r : α → α → Prop} {c : set α} (hc : is_chain r c) :
∃ (M : set α), is_max_chain r M c M

Every chain is contained in a maximal chain. This generalizes Hausdorff's maximality principle.