# 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:

- `(≤)` with `zorn_le`
- `(⊆)` 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 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.

source
theorem exists_maximal_of_chains_bounded {α : Type u_1} {r : α → α → Prop} (h : ∀ (c : Set α), IsChain r c → ∃ (ub : α), ∀ 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.

source
theorem exists_maximal_of_nonempty_chains_bounded {α : Type u_1} {r : α → α → Prop} [Nonempty α] (h : ∀ (c : Set α), IsChain r c → c.Nonempty → ∃ (ub : α), ∀ 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.

source
theorem zorn_le {α : Type u_1} [Preorder α] (h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) => x1 ≤ x2) c → BddAbove c) :
∃ (m : α), IsMax m
source
theorem zorn_le_nonempty {α : Type u_1} [Preorder α] [Nonempty α] (h : ∀ (c : Set α), IsChain (fun (x1 x2 : α) => x1 ≤ x2) c → c.Nonempty → BddAbove c) :
∃ (m : α), IsMax m
source
theorem zorn_le₀ {α : Type u_1} [Preorder α] (s : Set α) (ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) => x1 ≤ x2) c → ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) :
∃ (m : α), Maximal (fun (x : α) => x ∈ s) m
source
theorem zorn_le_nonempty₀ {α : Type u_1} [Preorder α] (s : Set α) (ih : ∀ c ⊆ s, IsChain (fun (x1 x2 : α) => x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub) (x : α) (hxs : x ∈ s) :
∃ (m : α), x ≤ m ∧ Maximal (fun (x : α) => x ∈ s) m
source
theorem zorn_le_nonempty_Ici₀ {α : Type u_1} [Preorder α] (a : α) (ih : ∀ c ⊆ Set.Ici a, IsChain (fun (x1 x2 : α) => x1 ≤ x2) c → ∀ y ∈ c, ∃ (ub : α), ∀ z ∈ c, z ≤ ub) (x : α) (hax : a ≤ x) :
∃ (m : α), x ≤ m ∧ IsMax m
source
theorem zorn_subset {α : Type u_1} (S : Set (Set α)) (h : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) :
∃ (m : Set α), Maximal (fun (x : Set α) => x ∈ S) m
source
theorem zorn_subset_nonempty {α : Type u_1} (S : Set (Set α)) (H : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c → c.Nonempty → ∃ ub ∈ S, ∀ s ∈ c, s ⊆ ub) (x : Set α) (hx : x ∈ S) :
∃ (m : Set α), x ⊆ m ∧ Maximal (fun (x : Set α) => x ∈ S) m
source
theorem zorn_superset {α : Type u_1} (S : Set (Set α)) (h : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) :
∃ (m : Set α), Minimal (fun (x : Set α) => x ∈ S) m
source
theorem zorn_superset_nonempty {α : Type u_1} (S : Set (Set α)) (H : ∀ c ⊆ S, IsChain (fun (x1 x2 : Set α) => x1 ⊆ x2) c → c.Nonempty → ∃ lb ∈ S, ∀ s ∈ c, lb ⊆ s) (x : Set α) (hx : x ∈ S) :
∃ m ⊆ x, Minimal (fun (x : Set α) => x ∈ S) m
source
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.

### Flags #

source
theorem IsChain.exists_subset_flag {α : Type u_1} [Preorder α] {c : Set α} (hc : IsChain (fun (x1 x2 : α) => x1 ≤ x2) c) :
∃ (s : Flag α), c ⊆ ↑s
source
theorem Flag.exists_mem {α : Type u_1} [Preorder α] (a : α) :
∃ (s : Flag α), a ∈ s
source
theorem Flag.exists_mem_mem {α : Type u_1} [Preorder α] {a b : α} (hab : a ≤ b) :
∃ (s : Flag α), a ∈ s ∧ b ∈ s
source
instance Flag.instNonempty {α : Type u_1} [Preorder α] :
Nonempty (Flag α)