edges_map

Mathlib.Combinatorics.SimpleGraph.Walk

URI: https://scilib.ai/kg/mathlib#SimpleGraph.Walk.edges_map

Lean4

@[simp]
theorem edges_map : (p.map f).edges = p.edges.map (Sym2.map f) := by
  induction p with
  | nil => rfl
  | cons _ _ ih => simp only [Walk.map_cons, edges_cons, List.map_cons, Sym2.map_pair_eq, ih]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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