set_walk_length_zero_eq_of_ne

Mathlib.Combinatorics.SimpleGraph.Connectivity.WalkCounting

URI: https://scilib.ai/kg/mathlib#SimpleGraph.set_walk_length_zero_eq_of_ne

← MathLib Explorer

English

If u ≠ v, there is no walk from u to v of length zero.

Русский

Если u ≠ v, то не существует ходa длины ноль от u до v.

LaTeX

$${p : G.Walk u v | p.length = 0} = ∅$$

Lean4

theorem set_walk_length_zero_eq_of_ne {u v : V} (h : u ≠ v) : {p : G.Walk u v | p.length = 0} = ∅ :=
  by
  ext p
  simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false]
  exact fun h' => absurd (Walk.eq_of_length_eq_zero h') h

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

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

Разделы

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

Аффилиация

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