nil_iff_support_eq

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

For any p, p.Nil is equivalent to p.support = [v].

Русский

Для любого p, p.Nil эквивалентно p.support = [v].

LaTeX

$$$ p.Nil \iff p.support = [v] $$$

Lean4

theorem nil_iff_support_eq {p : G.Walk v w} : p.Nil ↔ p.support = [v] := by cases p <;> simp

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

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

Разделы

Аффилиация

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