getLast_support

Mathlib.Combinatorics.SimpleGraph.Walk

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

← MathLib Explorer

English

The last element of the support of a walk equals its end vertex.

Русский

Последний элемент опоры пути равен его конечной вершине.

LaTeX

$$$p.\mathrm{support}.\mathrm{getLast} = \text{end}(p)$$$

Lean4

@[simp]
theorem getLast_support {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.getLast (by simp) = b :=
  by
  induction p
  · simp
  · simpa

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

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

Разделы

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

Аффилиация

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