isPath_iff_eq_nil

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

A walk from u to u is a path if and only if it is the nil walk.

Русский

Ход от u к u является путём тогда и только тогда, когда он нулевой обход.

LaTeX

$$$ p.IsPath \iff p = nil \quad (p:\\ G.Walk u u) $$$

Lean4

@[simp]
theorem isPath_iff_eq_nil {u : V} (p : G.Walk u u) : p.IsPath ↔ p = nil := by cases p <;> simp [IsPath.nil]

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

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

Разделы

Аффилиация

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