Documentation

Mathlib.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 an 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 (TODO: update to mathlib4)

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 α), IsChain r c∃ (ub : α), ac, r 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 α), IsChain r cSet.Nonempty c∃ (ub : α), ac, r 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_preorder {α : Type u_1} [Preorder α] (h : ∀ (c : Set α), IsChain (fun (x x_1 : α) => x x_1) cBddAbove c) :
∃ (m : α), ∀ (a : α), m aa m
theorem zorn_nonempty_preorder {α : Type u_1} [Preorder α] [Nonempty α] (h : ∀ (c : Set α), IsChain (fun (x x_1 : α) => x x_1) cSet.Nonempty cBddAbove c) :
∃ (m : α), ∀ (a : α), m aa m
theorem zorn_preorder₀ {α : Type u_1} [Preorder α] (s : Set α) (ih : cs, IsChain (fun (x x_1 : α) => x x_1) c∃ ub ∈ s, zc, z ub) :
∃ m ∈ s, zs, m zz m
theorem zorn_nonempty_preorder₀ {α : Type u_1} [Preorder α] (s : Set α) (ih : cs, IsChain (fun (x x_1 : α) => x x_1) cyc, ∃ ub ∈ s, zc, z ub) (x : α) (hxs : x s) :
∃ m ∈ s, x m zs, m zz m
theorem zorn_nonempty_Ici₀ {α : Type u_1} [Preorder α] (a : α) (ih : cSet.Ici a, IsChain (fun (x x_1 : α) => x x_1) cyc, ∃ (ub : α), zc, z ub) (x : α) (hax : a x) :
∃ (m : α), x m ∀ (z : α), m zz m
theorem zorn_partialOrder {α : Type u_1} [PartialOrder α] (h : ∀ (c : Set α), IsChain (fun (x x_1 : α) => x x_1) cBddAbove c) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn_nonempty_partialOrder {α : Type u_1} [PartialOrder α] [Nonempty α] (h : ∀ (c : Set α), IsChain (fun (x x_1 : α) => x x_1) cSet.Nonempty cBddAbove c) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn_partialOrder₀ {α : Type u_1} [PartialOrder α] (s : Set α) (ih : cs, IsChain (fun (x x_1 : α) => x x_1) c∃ ub ∈ s, zc, z ub) :
∃ m ∈ s, zs, m zz = m
theorem zorn_nonempty_partialOrder₀ {α : Type u_1} [PartialOrder α] (s : Set α) (ih : cs, IsChain (fun (x x_1 : α) => x x_1) cyc, ∃ ub ∈ s, zc, z ub) (x : α) (hxs : x s) :
∃ m ∈ s, x m zs, m zz = m
theorem zorn_subset {α : Type u_1} (S : Set (Set α)) (h : cS, IsChain (fun (x x_1 : Set α) => x x_1) c∃ ub ∈ S, sc, s ub) :
∃ m ∈ S, aS, m aa = m
theorem zorn_subset_nonempty {α : Type u_1} (S : Set (Set α)) (H : cS, IsChain (fun (x x_1 : Set α) => x x_1) cSet.Nonempty c∃ ub ∈ S, sc, s ub) (x : Set α) (hx : x S) :
∃ m ∈ S, x m aS, m aa = m
theorem zorn_superset {α : Type u_1} (S : Set (Set α)) (h : cS, IsChain (fun (x x_1 : Set α) => x x_1) c∃ lb ∈ S, sc, lb s) :
∃ m ∈ S, aS, a ma = m
theorem zorn_superset_nonempty {α : Type u_1} (S : Set (Set α)) (H : cS, IsChain (fun (x x_1 : Set α) => x x_1) cSet.Nonempty c∃ lb ∈ S, sc, lb s) (x : Set α) (hx : x S) :
∃ m ∈ S, m x aS, a ma = m
theorem IsChain.exists_maxChain {α : Type u_1} {r : ααProp} {c : Set α} (hc : IsChain r c) :
∃ (M : Set α), IsMaxChain r M c M

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