mathlib3 documentation

order.zorn

Zorn's lemmas #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 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 exists a maximal element.

theorem exists_maximal_of_nonempty_chains_bounded {α : Type u_1} {r : α α Prop} [nonempty α] (h : (c : set α), is_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

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_preorder {α : Type u_1} [preorder α] (h : (c : set α), is_chain has_le.le c bdd_above c) :
(m : α), (a : α), m a a m
theorem zorn_nonempty_preorder {α : Type u_1} [preorder α] [nonempty α] (h : (c : set α), is_chain has_le.le c c.nonempty bdd_above c) :
(m : α), (a : α), m a a m
theorem zorn_preorder₀ {α : Type u_1} [preorder α] (s : set α) (ih : (c : set α), c s is_chain has_le.le c ( (ub : α) (H : ub s), (z : α), z c z ub)) :
(m : α) (H : m s), (z : α), z s m z z m
theorem zorn_nonempty_preorder₀ {α : Type u_1} [preorder α] (s : set α) (ih : (c : set α), c s is_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
theorem zorn_nonempty_Ici₀ {α : Type u_1} [preorder α] (a : α) (ih : (c : set α), c set.Ici a is_chain has_le.le c (y : α), y c ( (ub : α), a ub (z : α), z c z ub)) (x : α) (hax : a x) :
(m : α), x m (z : α), m z z m
theorem zorn_partial_order {α : Type u_1} [partial_order α] (h : (c : set α), is_chain has_le.le c bdd_above c) :
(m : α), (a : α), m a a = m
theorem zorn_nonempty_partial_order {α : Type u_1} [partial_order α] [nonempty α] (h : (c : set α), is_chain has_le.le c c.nonempty bdd_above c) :
(m : α), (a : α), m a a = m
theorem zorn_partial_order₀ {α : Type u_1} [partial_order α] (s : set α) (ih : (c : set α), c s is_chain has_le.le c ( (ub : α) (H : ub s), (z : α), z c z ub)) :
(m : α) (H : m s), (z : α), z s m z z = m
theorem zorn_nonempty_partial_order₀ {α : Type u_1} [partial_order α] (s : set α) (ih : (c : set α), c s is_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
theorem zorn_subset {α : Type u_1} (S : set (set α)) (h : (c : set (set α)), c S is_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
theorem zorn_subset_nonempty {α : Type u_1} (S : set (set α)) (H : (c : set (set α)), c S is_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
theorem zorn_superset {α : Type u_1} (S : set (set α)) (h : (c : set (set α)), c S is_chain has_subset.subset c ( (lb : set α) (H : lb S), (s : set α), s c lb s)) :
(m : set α) (H : m S), (a : set α), a S a m a = m
theorem zorn_superset_nonempty {α : Type u_1} (S : set (set α)) (H : (c : set (set α)), c S is_chain has_subset.subset c c.nonempty ( (lb : set α) (H : lb S), (s : set α), s c lb s)) (x : set α) (hx : x S) :
(m : set α) (H : m S), m x (a : set α), a S a m a = 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.