English
For a finite set t, the non-clique-counting property is preserved by mapping along an embedding, provided t is nontrivial; the mapped graph has an NClique on t iff there exists a Finset s in α with G.IsNClique n s and s.map f = t.
Русский
При отображении через вложение сохраняется свойство IsNClique на конечном множестве t: существует Finset s в α такое, что G.IsNClique n s и s.map f = t, тогда (G.map f).IsNClique n t.
LaTeX
$$$$ (G.map\\ f).IsNClique\\ n\\ t \\iff \\exists s:\\ Finset\\ α,\\ G.IsNClique\\ n\\ s \\land s.map\\ f = t $$$$
Lean4
theorem isClique_map_finset_iff : (G.map f).IsClique t ↔ #t ≤ 1 ∨ ∃ (s : Finset α), G.IsClique s ∧ s.map f = t :=
by
obtain (ht | ht) := le_or_gt (#t) 1
· simp only [ht, true_or, iff_true]
exact IsClique.of_subsingleton <| card_le_one.1 ht
rw [isClique_map_finset_iff_of_nontrivial, ← not_lt]
· simp [ht]
exact Finset.one_lt_card_iff_nontrivial.mp ht
