cliqueFree_of_card_lt — Mathlib

English

The graph is not clique-free of size n if and only if the trivial graph on Fin n embeds into G.

Русский

Граф не clique-free на n тогда и только тогда, когда тривиальный граф на Fin n встраивается в G.

LaTeX

$$$ \neg G.CliqueFree(n) \iff \text{Nonempty}((\mathrm{completeGraph}(\mathrm{Fin} n)) \hookrightarrow G). $$$

Lean4

/-- See `SimpleGraph.cliqueFree_of_chromaticNumber_lt` for a tighter bound. -/
theorem cliqueFree_of_card_lt [Fintype α] (hc : card α < n) : G.CliqueFree n :=
  by
  rw [cliqueFree_iff]
  contrapose! hc
  simpa only [Fintype.card_fin] using Fintype.card_le_of_embedding hc.some.toEmbedding

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