not_nil_of_isCycle_cons — Mathlib

English

Let p be a walk from u to v and h an edge from v to u. If the walk obtained by prepending h to p forms a cycle, then p is not the nil walk.

Русский

Пусть p — ход из u в v и h — ребро между v и u. Если Walk.cons h p образует цикл, то p не является нулевым ходом.

LaTeX

$$(Walk.cons h p).IsCycle \Rightarrow p \neq Nil$$

Lean4

theorem not_nil_of_isCycle_cons {p : G.Walk u v} {h : G.Adj v u} (hc : (Walk.cons h p).IsCycle) : ¬p.Nil :=
  by
  have := Walk.length_cons _ _ ▸ Walk.IsCycle.three_le_length hc
  rw [Walk.not_nil_iff_lt_length]
  cutsat

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