adj_of_length_eq_one

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

If a walk p has length 1, then its endpoints are adjacent.

Русский

Если путь p имеет длину 1, то концы пути смежны.

LaTeX

$$$\forall {G,u,v,p}: G.Walk u v,\ \operatorname{length}(p) = 1 \Rightarrow G.Adj u v$$$

Lean4

theorem adj_of_length_eq_one {u v : V} : ∀ {p : G.Walk u v}, p.length = 1 → G.Adj u v
  | cons h nil, _ => h

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

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

Разделы

Аффилиация

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