not_nil

Mathlib.Combinatorics.SimpleGraph.Paths

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

English

For any p : G.Walk v v, IsCycle p implies p.Nil is false.

Русский

Для любого обхода p: G.Walk v v, если p является циклом, то p.Nil неверен (не пустой).

LaTeX

$$not_nil : ∀ {p : G.Walk v v}, IsCycle p → ¬ p.Nil$$

Lean4

theorem not_nil {p : G.Walk v v} (hp : IsCycle p) : ¬p.Nil :=
  (hp.ne_nil ·.eq_nil)

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

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

Разделы

Аффилиация

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