not_cliqueFree_card_of_top_embedding

English

If there exists a top embedding f : (⊤ : SimpleGraph α) ↪g G, then ¬G.CliqueFree(card α).

Русский

Если существует топ-встраивание f : ⊤ ↪g G, тогда G не clique-free для card α.

LaTeX

$$$ \text{not_cliqueFree_}\text{card_of_top_embedding} : \exists f : (\top : SimpleGraph(\mathrm{Fin} \alpha)) \hookrightarrow G, \neg G.CliqueFree(\mathrm{card}\,\alpha). $$$

Lean4

theorem not_cliqueFree_card_of_top_embedding [Fintype α] (f : (⊤ : SimpleGraph α) ↪g G) : ¬G.CliqueFree (card α) :=
  by
  rw [not_cliqueFree_iff]
  exact ⟨(Iso.completeGraph (Fintype.equivFin α)).symm.toEmbedding.trans f⟩

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