English
For an embedding f, a set s is a clique in G if and only if its image under f, namely f '' s, is a clique in the mapped graph G.map f.
Русский
Пусть имеется вложение f. Набор s является кликой графа G тогда и только тогда, когда образ f '' s является кликой графа G, полученного путём отображения посредством f.
LaTeX
$$$(G.map\\ f).IsClique(f'' s) \\iff G.IsClique(s)$$$
Lean4
@[simp]
theorem isClique_map_image_iff {f : α ↪ β} : (G.map f).IsClique (f '' s) ↔ G.IsClique s :=
by
rw [isClique_map_iff, f.injective.subsingleton_image_iff]
obtain (hs | hs) := s.subsingleton_or_nontrivial
· simp [hs, IsClique.of_subsingleton]
simp [or_iff_right hs.not_subsingleton, Set.image_eq_image f.injective]