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 by ... (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

lemma zorny_lemma : zorny_statement := by
  let s : Set α := {x | whatever x}
  suffices ∃ x ∈ s, ∀ y ∈ s, y ⊆ x → y = x by -- or with another operator xxx
    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⟩

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 cc.Nonempty∃ (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_le {α : Type u_1} [Preorder α] (h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) => x1 x2) cBddAbove c) :
∃ (m : α), IsMax m
theorem zorn_le_nonempty {α : Type u_1} [Preorder α] [Nonempty α] (h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) => x1 x2) cc.NonemptyBddAbove c) :
∃ (m : α), IsMax m
theorem zorn_le₀ {α : Type u_1} [Preorder α] (s : Set α) (ih : cs, IsChain (fun (x1 x2 : α) => x1 x2) cubs, zc, z ub) :
∃ (m : α), Maximal (fun (x : α) => x s) m
theorem zorn_le_nonempty₀ {α : Type u_1} [Preorder α] (s : Set α) (ih : cs, IsChain (fun (x1 x2 : α) => x1 x2) cyc, ubs, zc, z ub) (x : α) (hxs : x s) :
∃ (m : α), x m Maximal (fun (x : α) => x s) m
theorem zorn_le_nonempty_Ici₀ {α : Type u_1} [Preorder α] (a : α) (ih : cSet.Ici a, IsChain (fun (x1 x2 : α) => x1 x2) cyc, ∃ (ub : α), zc, z ub) (x : α) (hax : a x) :
∃ (m : α), x m IsMax m
theorem zorn_subset {α : Type u_1} (S : Set (Set α)) (h : cS, IsChain (fun (x1 x2 : Set α) => x1 x2) cubS, sc, s ub) :
∃ (m : Set α), Maximal (fun (x : Set α) => x S) m
theorem zorn_subset_nonempty {α : Type u_1} (S : Set (Set α)) (H : cS, IsChain (fun (x1 x2 : Set α) => x1 x2) cc.NonemptyubS, sc, s ub) (x : Set α) (hx : x S) :
∃ (m : Set α), x m Maximal (fun (x : Set α) => x S) m
theorem zorn_superset {α : Type u_1} (S : Set (Set α)) (h : cS, IsChain (fun (x1 x2 : Set α) => x1 x2) clbS, sc, lb s) :
∃ (m : Set α), Minimal (fun (x : Set α) => x S) m
theorem zorn_superset_nonempty {α : Type u_1} (S : Set (Set α)) (H : cS, IsChain (fun (x1 x2 : Set α) => x1 x2) cc.NonemptylbS, sc, lb s) (x : Set α) (hx : x S) :
mx, Minimal (fun (x : Set α) => x S) 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.