Mathlib theorem · Existing formal mathematics
ProofAtlas

Existing in Mathlib · Logic and foundations

Zorn’s Lemma

Suppose every totally ordered collection of objects has some common upper bound. Then there is an object that cannot be moved strictly upward: anything above it is also below it.

Exact theorem

Exact Mathlib statement

theorem zorn_le {α : Type*} [Preorder α] (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) : ∃ m : α, IsMax m

The theorem at a glance

Zorn’s Lemma at a glance

A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.

If every chain in a preorder has an upper bound, the preorder has a maximal element. Explanatory diagram.
Detailed visual description

The poster centers the all-chains hypothesis and maximal-element conclusion. Its proof route selects a maximal chain, bounds it, tests an attempted extension, and uses maximal-chain closure to force a return relation. The footer separates maximal from greatest and equality.

Statement structure

From hypotheses to conclusion

Statement map for Zorn’s LemmaIn a preorder where every chain is bounded above, a maximal element exists. The pinned upstream declaration is zorn_le. The exact checked statement is theorem zorn_le {α : Type*} [Preorder α] (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) : ∃ m : α, IsMax m.Mathematical readingIn a preorder whereevery chain is boundedabove, a maximal elementexists.Pinned declarationmathlib · zorn_leExact checked formtheorem zorn_le {α :Type*} [Preorder α] (h :∀ c : Set α, IsChain (·≤ ·) c → BddAbove c) : ∃m : α, IsMax mStatement map for Zorn’s LemmaIn a preorder where every chain is bounded above, a maximal element exists. The pinned upstream declaration is zorn_le. The exact checked statement is theorem zorn_le {α : Type*} [Preorder α] (h : ∀ c : Set α, IsChain (· ≤ ·) c → BddAbove c) : ∃ m : α, IsMax m.Mathematical readingIn a preorder whereevery chain is boundedabove, a maximal elementexists.Pinned declarationmathlib · zorn_leExact checked formtheorem zorn_le {α :Type*} [Preorder α] (h :∀ c : Set α, IsChain (·≤ ·) c → BddAbove c) : ∃m : α, IsMax m

This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.

Bounding every chain yields a maximal element, not necessarily a greatest one. Explanatory diagram.
Detailed visual description

A gold chain threads through a wide branching preorder and ends beneath one luminous upper bound. Any attempted point above that bound carries a return relation, expressing mutual comparability rather than equality, while side branches remain incomparable and extend outside the bound's reach.

Why it matters

A mathematical landmark

Zorn's lemma is one of the central maximality forms of the axiom of choice and a ubiquitous engine for existence proofs across algebra, analysis, and topology. Mathlib's selected endpoint is stated for preorders, so maximality is deliberately weaker than being a greatest element.

ProofAtlas record

What has been checked

Upstream indexedPinned source bytes verified locally
Locally reproducedExact upstream declaration replayed
Reviewed pageCurrent public presentation reviewed
Accepted Atlas resultNot recorded for the preferred artifact

Mathlib is the source of the theorem; the local Lean replay and page review are separate.

Claim boundary

No new theorem is claimed

This target indexes Mathlib's preorder specialization of Zorn's lemma: every set-valued chain, including the empty chain, is bounded above, and the conclusion is an IsMax element. It does not produce a greatest element, uniqueness, a constructive search, or maximality inside a designated subset.

Source and local evidence

Where the theorem comes from

Existing declaration
zorn_le in mathlib
Relationship
The checked artifact is the upstream declaration itself
Local Lean evidence
artifact.library.mathlib.zorn-lemma.v001
Source
Open the pinned upstream reference