not_nil_of_tail_not_nil

Mathlib.Combinatorics.SimpleGraph.Walk

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

English

If the tail of p is nonempty, then p is nonempty.

Русский

Если хвост хода p непустой, то сам ход непустой.

LaTeX

$$$ p.tail \\neq Nil \\rightarrow p \\neq Nil $$$

Lean4

theorem not_nil_of_tail_not_nil {p : G.Walk v w} (hp : ¬p.tail.Nil) : ¬p.Nil :=
  mt Nil.tail hp

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

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

Разделы

Аффилиация

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