edgeSet_transfer

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

Edges of a transferred walk equal the original edges, transferred via a suitable map.

Русский

Рёбра перенесённого обхода соответствуют исходным рёбрам, перенесённым через соответствующее отображение.

LaTeX

$$(p.transfer H hp).edgeSet = p.edgeSet$$

Lean4

@[simp]
theorem edgeSet_transfer (hp) : (p.transfer H hp).edgeSet = p.edgeSet := by ext; simp

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

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

Разделы

Аффилиация

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