English
A witness that a graph is not clique-free gives a top embedding of a complete graph on Fin n into G.
Русский
Свидетель того, что граф не clique-free, задаёт верхнее вложение полного графа на Fin n в G.
LaTeX
$$$ \exists f : (\top : SimpleGraph(Fin n)) \hookrightarrow G, \text{ witness variables }. $$$
Lean4
theorem not_cliqueFree_of_top_embedding {n : ℕ} (f : (⊤ : SimpleGraph (Fin n)) ↪g G) : ¬G.CliqueFree n :=
by
simp only [CliqueFree, isNClique_iff, isClique_iff_induce_eq, not_forall, Classical.not_not]
use Finset.univ.map f.toEmbedding
simp only [card_map, Finset.card_fin, and_true]
ext ⟨v, hv⟩ ⟨w, hw⟩
simp only [coe_map, Set.mem_image, coe_univ, Set.mem_univ, true_and] at hv hw
obtain ⟨v', rfl⟩ := hv
obtain ⟨w', rfl⟩ := hw
simp_rw [RelEmbedding.coe_toEmbedding, comap_adj, Function.Embedding.coe_subtype, f.map_adj_iff, top_adj, ne_eq,
Subtype.mk.injEq, RelEmbedding.inj]
