of_subsingleton

Mathlib.Combinatorics.SimpleGraph.Clique

URI: https://scilib.ai/kg/mathlib#SimpleGraph.IsClique.of_subsingleton

English

If s is a clique in G, then its image under an embedding f is a clique in the mapped graph.

Русский

Если s — клика в G, то образ подотражения f является кликой в графе, получаемом применением map.

LaTeX

$$$ G.IsClique s \rightarrow (G.map f).IsClique (f '' s) $$$

Lean4

theorem of_subsingleton {G : SimpleGraph α} (hs : s.Subsingleton) : G.IsClique s :=
  hs.pairwise G.Adj

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru