English
If r ≤ |V| and G is Turán-maximal for r, then G is not r-clique-free (i.e., G contains an r-clique).
Русский
Если r ≤ |V| и G — Турэнмаксима для r, то G не является r-полным без клики, то есть в нём есть клика размера r.
LaTeX
$$$\forall V, r, \ hn: r \le |V| \land G^{\mathrm{IsTuranMaximal}}(r) \implies \neg (G \mathrm{CliqueFree}(r)).$$$
Lean4
/-- An `r + 1`-cliquefree Turán-maximal graph is _not_ `r`-cliquefree
if it can accommodate such a clique. -/
theorem not_cliqueFree_of_isTuranMaximal (hn : r ≤ Fintype.card V) (hG : G.IsTuranMaximal r) : ¬G.CliqueFree r :=
by
rintro h
obtain ⟨K, _, rfl⟩ := exists_subset_card_eq hn
obtain ⟨a, -, b, -, hab, hGab⟩ : ∃ a ∈ K, ∃ b ∈ K, a ≠ b ∧ ¬G.Adj a b := by
simpa only [isNClique_iff, IsClique, Set.Pairwise, mem_coe, ne_eq, and_true, not_forall, exists_prop,
exists_and_right] using h K
exact
hGab <|
le_sup_right.trans_eq ((hG.le_iff_eq <| h.sup_edge _ _).1 le_sup_left).symm <|
(edge_adj ..).2 ⟨Or.inl ⟨rfl, rfl⟩, hab⟩
