isClique_map_image_iff — Mathlib

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]

Похожие утверждения