Given any attempted list of all subsets of a type, form the subset that reverses membership at each element's own listed position. That diagonal subset cannot appear anywhere in the list.
Accepted Atlas resultNot recorded for the preferred artifact
These states distinguish upstream identity, local reproduction, review, and Atlas acceptance. This page is part of the public, read-only Mathlib landmark collection.
Formal orientation
Statement map
This deterministic map orients the reader from the mathematical summary to the pinned declaration and exact checked form. The HTML statement below is authoritative.
The theorem at a glance
Cantor's Theorem at a glance
A source-bound editorial overview of the exact Mathlib formulation. The image is explanatory; the statement map, formal type, and pinned source remain authoritative.
No mapping from a type reaches every subset of that same type. Generated explanation only; the exact HTML statement and pinned source are authoritative.Detailed visual description
The poster makes the hypothetical enumeration, the diagonal subset, and the complement fixed-point contradiction explicit while keeping the formal endpoint at non-surjectivity onto Set α.
Cantor's Theorem schematic
Loading full-resolution image…
The diagonal subset reverses membership at each proposed preimage, so no enumeration reaches every subset.Open original image in a new tab ↗
The diagonal subset reverses membership at each proposed preimage, so no enumeration reaches every subset. Generated explanation only; the exact HTML statement and pinned source are authoritative.Detailed visual description
A single mapping tapestry connects source elements to candidate subsets. The gold diagonal construction follows those assignments and reverses each self-membership decision, making its own subset unavailable as an image of the function.
Complementary intuition
A mathematical landmark
Cantor's diagonal argument transformed the study of infinity and became a reusable template across logic, computability, and mathematics. The selected Mathlib theorem captures the exact non-surjectivity statement.
The low-text schematic gives the theorem a visual identity; it does not replace the source-bound poster or exact statement.
Authoritative formal type
Exact Mathlib statement
theorem Function.cantor_surjective {α : Type*} (f : α → Set α) : ¬Function.Surjective f
Selected evidence declaration text
theorem Function.cantor_surjective {α : Type*} (f : α → Set α) : ¬Function.Surjective f
Proof architecture
Cantor's diagonal contradiction
2 curated stages
Mathlib proves that no function from a type to its power set is surjective by first showing that a hypothetical surjective family would force every endofunction to have a fixed point, then applying that bridge to complementation, which has no fixed point.
These source-anchored stages explain the retained Mathlib proof route. They are generated explanations, not proof evidence or an extracted Lean proof-term dependency graph.
01
A surjection would force every endofunction to have a fixed point
A surjection would force every endofunction to have a fixed point
Loading full-resolution image…
Evaluating a surjective family on its own index constructs an element fixed by any chosen endofunction.Open original image in a new tab ↗
Evaluating a surjective family on its own index constructs an element fixed by any chosen endofunction.
Surjective f → ∀ g : β → β, ∃ x, g x = x
The checked helper exists_fixed_point_of_surjective assumes that a family f : α → α → β is surjective. For an endofunction g : β → β, surjectivity selects an index for the diagonal function a ↦ g (f a a); evaluating at that index produces a fixed point of g.
02
Complementation reverses membership at the diagonal
Complementation reverses membership at the diagonal
Loading full-resolution image…
Applying the fixed-point bridge to set complementation would make a subset equal to its own complement, an impossibility.Open original image in a new tab ↗
Applying the fixed-point bridge to set complementation would make a subset equal to its own complement, an impossibility.
∀ (f : α → Set α), ¬ Function.Surjective f
Function.cantor_surjective feeds the hypothetical surjection f : α → Set α and complementation into the helper. The resulting equality would identify a set with its complement, so not_iff_self closes the contradiction and rejects surjectivity.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's diagonal theorem that no function from a type to its power set is surjective. It does not separately state the cardinal inequality or claim a new proof.
Proof Atlas did not originate Cantor's Theorem or Mathlib's declaration.
The selected declaration is non-surjectivity onto Set α, not a separately stated cardinal inequality or an assertion that no functions exist.
The generated explanation and visuals are not proof evidence.
