Theorems · Theorem · combinatorics

SimpleGraph.colorable_of_cliqueFree_lt_minDegree

∀ {α : Type u_1} {G : SimpleGraph α} {r : ℕ} [inst : Fintype α] [inst_1 : DecidableRel G.Adj],
  G.CliqueFree (r + 1) → (3 * r - 4) * Fintype.card α / (3 * r - 1) < G.minDegree → G.Colorable r

Andrásfai-Erdős-Sós theorem If G is a Kᵣ₊₁-free graph with n vertices and (3 * r - 4) * n / (3 * r - 1) < G.minDegree then G is r + 1-colorable, e.g. if G is K₃-free and 2 * n / 5 < G.minDegree then G is 2-colorable.

Defined in

Mathlib.Combinatorics.SimpleGraph.FiveWheelLike

Cited by

0 results in Mathlib

Foundations

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

Assumes

FintypeDecidableRel