comap_map_eq

Mathlib.Combinatorics.SimpleGraph.Maps

URI: https://scilib.ai/kg/mathlib#SimpleGraph.comap_map_eq

English

For any embedding f: V ↪ W, mapping by f and then comapping by f yields back the original graph: (G.map f).comap f = G.

Русский

Для вложения f: V ↪ W отображение графа G по f затем комап по f возвращает исходный граф: (G.map f).comap f = G.

LaTeX

$$$$ (G.map f).comap f = G $$$$

Lean4

@[simp]
theorem comap_map_eq (f : V ↪ W) (G : SimpleGraph V) : (G.map f).comap f = G :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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