English
Let f be an embedding f: α ↪ β and t a subset of β. Then t is a clique in the graph G mapped along f if and only if either t has at most one element (is a subsingleton) or there exists a subset s of α such that s is a clique in G and f '' s = t.
Русский
Пусть f: α ↪ β — вложение, и t ⊆ β. Тогда t является кликой графа G, отображённого через f, тогда и только тогда либо t состоит не более чем из одного элемента, либо существует подмножество s ⊆ α такое, что s является кликой графа G и образ этого подмножества через f равен t.
LaTeX
$$$(G.map\; f).IsClique(t) \\iff t.Subsingleton \\lor \\exists s:\\ Set\\;\\alpha,\, G.IsClique(s) \\land f '' s = t$$$
Lean4
theorem isClique_map_iff {f : α ↪ β} {t : Set β} :
(G.map f).IsClique t ↔ t.Subsingleton ∨ ∃ (s : Set α), G.IsClique s ∧ f '' s = t :=
by
obtain (ht | ht) := t.subsingleton_or_nontrivial
· simp [IsClique.of_subsingleton, ht]
simp [isClique_map_iff_of_nontrivial ht, ht.not_subsingleton]
