cliqueFree_completeMultipartiteGraph

English

A complete r-partite graph has no n-cliques for r < n.

Русский

Полный граф с разбивкой на r частей не имеет n-клик, если r < n.

LaTeX

$$$ (\text{for } ι, V: ι \to \text{Type}) \ (card\,ι < n) \Rightarrow (\mathrm{completeMultipartiteGraph}(V)).IsNClique(n) = \text{false}. $$$

Lean4

/-- A complete `r`-partite graph has no `n`-cliques for `r < n`. -/
theorem cliqueFree_completeMultipartiteGraph {ι : Type*} [Fintype ι] (V : ι → Type*) (hc : card ι < n) :
    (completeMultipartiteGraph V).CliqueFree n :=
  by
  rw [cliqueFree_iff, isEmpty_iff]
  intro f
  obtain ⟨v, w, hn, he⟩ := exists_ne_map_eq_of_card_lt (Sigma.fst ∘ f) (by simp [hc])
  rw [← top_adj, ← f.map_adj_iff, comap_adj, top_adj] at hn
  exact absurd he hn

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