isNClique_map_copy_top — Mathlib

English

A copy of the complete graph on β embedded in G yields a clique of size card β in G.

Русский

Копия полного графа на β, вложенная в G, образует клику размерности card β в G.

LaTeX

$$$ G.IsNClique(\operatorname{card} \beta, \mathrm{univ}.map f.toEmbedding). $$$

Lean4

/-- The vertices in a copy of `⊤ : SimpleGraph β` are a `card β`-clique. -/
theorem isNClique_map_copy_top [Fintype β] (f : Copy (⊤ : SimpleGraph β) G) :
    G.IsNClique (card β) (univ.map f.toEmbedding) :=
  by
  rw [isNClique_iff, card_map, card_univ, coe_map, coe_univ, Set.image_univ]
  exact ⟨isClique_range_copy_top f, rfl⟩

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