Theorems · Theorem · combinatorics

SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph

• 1000+ list: Turán's theorem

∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {r : ℕ},
  0 < r → (G.IsTuranMaximal r ↔ Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) r))

Turán's theorem. turanGraph n r is, up to isomorphism, the unique r + 1-cliquefree Turán-maximal graph on n vertices.

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Cited by

2 results in Mathlib

Foundations

Depth 90 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeDecidableRel