support_reverse

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

For any walk p, the last element of its support equals the end vertex of p.

Русский

Для любого пути p последняя вершина опоры равна конечной вершине p.

LaTeX

$$$p.\mathrm{support}.\mathrm{getLast} = b$ для p : G.Walk a b$$

Lean4

@[simp]
theorem support_reverse {u v : V} (p : G.Walk u v) : p.reverse.support = p.support.reverse := by
  induction p <;> simp [support_append, *]

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

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

Разделы

Аффилиация

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