map_adj

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Hom.map_adj

English

A graph homomorphism preserves adjacency: if v is adjacent to w in G, then f(v) is adjacent to f(w) in G'.

Русский

Гомоморфизм графа сохраняет смежность: если v смежен с w в G, то f(v) смежен с f(w) в G'.

LaTeX

$$$ G.Adj\\; v\\; w \\Rightarrow G'.Adj\\; (f(v))\\;(f(w)) $$$

Lean4

theorem map_adj {v w : V} (h : G.Adj v w) : G'.Adj (f v) (f w) :=
  f.map_rel' h

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

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

Разделы

Аффилиация

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