head_support

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

For any walk p : G.Walk a b, the head of its support is a.

Русский

Для любого пути p: G.Walk a b голова опоры равна a.

LaTeX

$$$p.\mathrm{support}.\mathrm{head} = a$$$

Lean4

@[simp]
theorem head_support {G : SimpleGraph V} {a b : V} (p : G.Walk a b) : p.support.head (by simp) = a := by
  cases p <;> simp

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

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

Разделы

Аффилиация

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