map_comp

Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

URI: https://scilib.ai/kg/mathlib#SimpleGraph.ConnectedComponent.map_comp

Lean4

@[simp]
theorem map_comp (C : G.ConnectedComponent) (φ : G →g G') (ψ : G' →g G'') : (C.map φ).map ψ = C.map (ψ.comp φ) :=
  C.ind (fun _ => rfl)

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

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

Разделы

Аффилиация

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