eq_of_length_eq_zero

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

If a walk p from u to v has length zero, then u = v.

Русский

Если путь p из u в v имеет нулевую длину, то u = v.

LaTeX

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

Lean4

theorem eq_of_length_eq_zero {u v : V} : ∀ {p : G.Walk u v}, p.length = 0 → u = v
  | nil, _ => rfl

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

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

Разделы

Аффилиация

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