turanGraph_cliqueFree — Mathlib

English

If 0 < r, then the Turán graph on n vertices is free of (r+1)-cliques.

Русский

Если 0 < r, граф Турэна на n вершинах не содержит клики размера r+1.

LaTeX

$$$0 < r \Rightarrow (\mathrm{turanGraph}\, n\, r).\mathrm{CliqueFree}(r+1).$$$

Lean4

theorem turanGraph_cliqueFree (hr : 0 < r) : (turanGraph n r).CliqueFree (r + 1) :=
  by
  rw [cliqueFree_iff]
  by_contra! h
  obtain ⟨f, ha⟩ := h
  simp only [turanGraph, top_adj] at ha
  obtain ⟨x, y, d, c⟩ :=
    Fintype.exists_ne_map_eq_of_card_lt (fun x ↦ (⟨(f x).1 % r, Nat.mod_lt _ hr⟩ : Fin r)) (by simp)
  simp only [Fin.mk.injEq] at c
  exact absurd c ((@ha x y).mpr d)

Похожие утверждения