English
There exists a top embedding witnessing not_cliqueFree; i.e., a witness that there is a copy of a finite complete graph inside G.
Русский
Существует верхнее вложение, подтверждающее неclique-free; то есть копия полного графа внутри G.
LaTeX
$$$ \exists f : (\top : SimpleGraph( Fin n)) \hookrightarrow G. $$$
Lean4
@[simp]
theorem cliqueFree_map_iff {f : α ↪ β} [Nonempty α] : (G.map f).CliqueFree n ↔ G.CliqueFree n :=
by
obtain (hle | hlt) := le_or_gt n 1
· obtain (rfl | rfl) := Nat.le_one_iff_eq_zero_or_eq_one.1 hle
· simp [CliqueFree]
simp [CliqueFree, show ∃ (_ : β), True from ⟨f (Classical.arbitrary _), trivial⟩]
simp [CliqueFree, isNClique_map_iff hlt]