support_map

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

The list of darts (edge-directions) of a mapped walk is obtained by mapping each edge dart along f.

Русский

Список стрелок обхода после отображения получается путём отображения каждой дуги ребра через f.

LaTeX

$$$(p.map f).darts = \\text{List}.map\\, f.mapDart\\, p.darts$$$

Lean4

@[simp]
theorem support_map : (p.map f).support = p.support.map f := by induction p <;> simp [*]

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

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

Разделы

Аффилиация

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