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 #

• chain c: A chain c is a set of comparable elements.
• max_chain_spec: Hausdorff's Maximality Principle.
• exists_maximal_of_chains_bounded: Zorn's Lemma. Many variants are offered.

## Variants #

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

• (≤) with zorn_partial_order
• (⊆) with zorn_subset
• (⊇) with zorn_superset

Lemma names carry modifiers:

• ₀: Quantifies over a set, as opposed to over a type.
• _nonempty: Doesn't ask to prove that the empty chain is bounded and lets you give an element that will be smaller than the maximal element found (the maximal element is no smaller than any other element, but it can also be incomparable to some).

## 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} [ r] {c : set α} (H : 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' c c c'
theorem zorn.chain_of_trichotomous {α : Type u} {r : α → α → Prop} [ r] (s : set α) :
s
theorem zorn.chain_univ_iff {α : Type u} {r : α → α → Prop} :
theorem zorn.chain.directed_on {α : Type u} {r : α → α → Prop} [ r] {c : set α} (H : c) :
c
theorem zorn.chain_insert {α : Type u} {r : α → α → Prop} {c : set α} {a : α} (hc : c) (ha : ∀ (b : α), b cb ar a b r b a) :
(insert a c)
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 α), c c') :
theorem zorn.chain_succ {α : Type u} {r : α → α → Prop} {c : set α} (hc : c) :
theorem zorn.super_of_not_max {α : Type u} {r : α → α → Prop} {c : set α} (hc₁ : c) (hc₂ : ¬) :
theorem zorn.succ_increasing {α : Type u} {r : α → α → Prop} {c : set α} :
inductive zorn.chain_closure {α : Type u} {r : α → α → Prop} :
set (set α)
• succ : ∀ {α : Type u} {r : α → α → Prop} {s : set α},
• union : ∀ {α : Type u} {r : α → α → Prop} {s : set (set α)}, (∀ (a : set α), a s

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 : = 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) :
c
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 α), 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 α), 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 : s) :

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

theorem zorn.zorn_partial_order {α : Type u} (h : ∀ (c : set α), (∃ (ub : α), ∀ (a : α), a ca ub)) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn.zorn_nonempty_partial_order {α : Type u} [nonempty α] (h : ∀ (c : set α), c.nonempty(∃ (ub : α), ∀ (a : α), a ca ub)) :
∃ (m : α), ∀ (a : α), m aa = m
theorem zorn.zorn_partial_order₀ {α : Type u} (s : set α) (ih : ∀ (c : set α), c s(∃ (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} (s : set α) (ih : ∀ (c : set α), c s∀ (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 S(∃ (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 Sc.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 S(∃ (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 Sc.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 : 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 : c) :
(f '' c)
theorem directed_of_chain {α : Type u_1} {β : Type u_2} {r : β → β → Prop} [ r] {f : α → β} {c : set α} (h : zorn.chain (f ⁻¹'o r) c) :
(λ (x : {a // a c}), f x)