Theorems · Theorem · combinatorics

SimpleGraph.card_edgeFinset_eq_extremalNumber_top_iff_nonempty_iso_turanGraph

∀ {V : Type u_1} [inst : Fintype V] {G : SimpleGraph V} [inst_1 : DecidableRel G.Adj] {α : Type u_2}
  [inst_2 : Fintype α] [Nontrivial α],
  ⊤.Free G ∧ G.edgeFinset.card = SimpleGraph.extremalNumber (Fintype.card V) ⊤ ↔
    Nonempty (G ≃g SimpleGraph.turanGraph (Fintype.card V) (Fintype.card α - 1))

The turanGraph is, up to isomorphism, the unique extremal graph forbidding ⊤. This is Turán's theorem restated in terms of the extremal numbers of ⊤. See SimpleGraph.isTuranMaximal_iff_nonempty_iso_turanGraph.

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Turan

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRelFintypeNontrivial