Mathlib theorem · Existing formal mathematics
ProofAtlas

Existing in Mathlib · Combinatorics

Turán’s Theorem

For r > 0, among finite graphs on the same vertices that avoid a clique of size r+1, the edge-maximizers are precisely the balanced complete r-partite graphs, up to relabelling.

Exact theorem

Exact Mathlib statement

theorem SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph {V : Type*} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hr : 0 < r) : G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r)

The theorem at a glance

Turán’s Theorem at a glance

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

Zykov symmetrization forces nonadjacency classes, complete multipartite structure, balanced parts, and finally the Turán graph up to isomorphism. Explanatory diagram.
Detailed visual description

A balanced tripartite graph anchors the poster. The proof route moves from symmetric replacement of nonadjacent vertices to equivalence classes, equipartition, and an explicit graph isomorphism, while a boundary strip preserves maximum-edge rather than inclusion-maximal semantics.

Statement structure

From hypotheses to conclusion

Statement map for Turán’s TheoremFor r > 0, a finite graph has the maximum possible number of edges without an (r+1)-clique exactly when it is isomorphic to the balanced complete r-partite Turán graph. The pinned upstream declaration is SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph. The exact checked statement is theorem SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph {V : Type*} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hr : 0 < r) : G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r).Mathematical readingFor r > 0, a finitegraph has the maximumpossible number of edgeswithout an (r+1)-cliqueexactly when it isisomorphic to thebalanced completer-partite Turán graph.Pinned declarationmathlib ·SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraphExact checked formtheoremSimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph{V : Type*} [Fintype V]{G : SimpleGraph V}[DecidableRel G.Adj] {r: ℕ} (hr : 0 < r) :G.IsTuranMaximal r ↔Nonempty (G ≃gSimpleGraph.turanGraph(Fintype.card V) r)Statement map for Turán’s TheoremFor r > 0, a finite graph has the maximum possible number of edges without an (r+1)-clique exactly when it is isomorphic to the balanced complete r-partite Turán graph. The pinned upstream declaration is SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph. The exact checked statement is theorem SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph {V : Type*} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] {r : ℕ} (hr : 0 < r) : G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r).Mathematical readingFor r > 0, a finitegraph has the maximumpossible number of edgeswithout an (r+1)-cliqueexactly when it isisomorphic to thebalanced completer-partite Turán graph.Pinned declarationmathlib ·SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraphExact checked formtheoremSimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph{V : Type*} [Fintype V]{G : SimpleGraph V}[DecidableRel G.Adj] {r: ℕ} (hr : 0 < r) :G.IsTuranMaximal r ↔Nonempty (G ≃gSimpleGraph.turanGraph(Fintype.card V) r)

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

For r > 0, maximum-edge (r+1)-clique-free graphs are exactly the balanced complete r-partite Turán graphs, up to isomorphism. Explanatory diagram.
Detailed visual description

A concrete r=3 example shows the same nine-vertex graph before and after a part-preserving reorganization. The clean endpoint exposes three equal independent classes, complete cross-part adjacency, and the exclusion of a four-clique.

Why it matters

A mathematical landmark

Turán’s theorem founded extremal graph theory. The selected Mathlib endpoint gives a complete structural classification of the maximum-edge graphs, while the source proof exposes Zykov symmetrization, multipartite structure, and equipartition.

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 page indexes Mathlib’s structural Turán endpoint for finite simple graphs and positive r. IsTuranMaximal means maximum edge count among all (r+1)-clique-free graphs on the same finite vertex type, not merely inclusion-maximal. The conclusion is graph isomorphism to the balanced complete r-partite Turán graph, not literal equality of labelled graphs or uniqueness of the isomorphism. The selected declaration does not itself display the numerical edge formula.

Source and local evidence

Where the theorem comes from

Existing declaration
SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph in mathlib
Relationship
The checked artifact is the upstream declaration itself
Local Lean evidence
artifact.library.mathlib.turan-theorem.v001
Source
Open the pinned upstream reference