not_cliqueFree_of_le_enatCard — Mathlib

English

If ι is infinite, the complete multipartite graph on V cannot be clique-free for n.

Русский

Если ι бесконечен, то completeMultipartiteGraph(V) не clique-free для n.

LaTeX

$$$ \text{not_cliqueFree_of_infinite} : (\text{Infinite } ι) \Rightarrow \neg (\mathrm{completeMultipartiteGraph}(V).IsNClique(n)). $$$

Lean4

theorem not_cliqueFree_of_le_enatCard (f : ∀ (i : ι), V i) (hc : n ≤ ENat.card ι) :
    ¬(completeMultipartiteGraph V).CliqueFree n :=
  by
  by_cases h : Infinite ι
  · exact not_cliqueFree_of_infinite V f
  · have : Fintype ι := fintypeOfNotInfinite h
    rw [ENat.card_eq_coe_fintype_card, Nat.cast_le] at hc
    exact not_cliqueFree_of_le_card V f hc

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