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⟩