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

• (≤) with zorn_partialOrder
• (⊆) 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 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


Originally ported from Isabelle/HOL. The original file was written by Jacques D. Fleuriot, Tobias Nipkow, Christian Sternagel.