not_nil_cons

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

For any adjacent edge h and walk p, the constructed walk q = p.cons h is not Nil.

Русский

Пусть h — смежное ребро, а p — ход; тогда q = p.cons h не равен Nil.

LaTeX

$$$ \neg( (q \text{.cons} h).Nil ) $$$

Lean4

@[simp]
theorem not_nil_cons {h : G.Adj u v} {p : G.Walk v w} : ¬(cons h p).Nil :=
  nofun

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

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

Разделы

Аффилиация

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