not_cliqueFree_of_le_card — Mathlib

English

If there is a finite index set with cardinal less or equal the bound, the complete multipartite graph is not clique-free.

Русский

Если кардинал множества индексов не превосходит заданной величины, полный мультитип граф не clique-free.

LaTeX

$$$ \text{not_cliqueFree_of_le_card} : [Fintype ι] (V) (hc : n ≤ card ι) \Rightarrow \neg (\mathrm{completeMultipartiteGraph} V).IsNClique(n). $$$

Lean4

theorem not_cliqueFree_of_le_card [Fintype ι] (f : ∀ (i : ι), V i) (hc : n ≤ Fintype.card ι) :
    ¬(completeMultipartiteGraph V).CliqueFree n := fun hf ↦
  (cliqueFree_iff.1 <| hf.mono hc).elim' <|
    (topEmbedding V f).comp (Iso.completeGraph (Fintype.equivFin ι).symm).toEmbedding

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