support_eq_cons

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

The support of a walk p is the head element followed by the tail of the rest: p.support = a :: p.support.tail.

Русский

Опора пути p равна a, за которым следует хвост опоры: p.support = a :: p.support.tail.

LaTeX

$$$p.\mathrm{support} = a \;::\; p.\mathrm{support}.\mathrm{tail}$$$

Lean4

theorem support_eq_cons {u v : V} (p : G.Walk u v) : p.support = u :: p.support.tail := by cases p <;> simp

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

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

Разделы

Аффилиация

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