Theorems · Theorem · combinatorics

SimpleGraph.isExtremal_free_iff

∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {H : SimpleGraph W} [inst : Fintype V]
  [inst_1 : DecidableRel G.Adj],
  G.IsExtremal H.Free ↔ H.Free G ∧ G.edgeFinset.card = SimpleGraph.extremalNumber (Fintype.card V) H

H-free extremal graphs are H-free simple graphs having extremalNumber (card V) H many edges.

Defined in

Mathlib.Combinatorics.SimpleGraph.Extremal.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRel