adj_penultimate — Mathlib

English

Nonempty walks have their penultimate vertex adjacent to the final vertex.

Русский

Непустые ходы имеют, что их предпоследняя вершина смежна с последней вершиной.

LaTeX

$$$ p \\neq Nil \\rightarrow G.Adj\\ (p.penultimate)\\ w $$$

Lean4

@[simp]
theorem adj_penultimate {p : G.Walk v w} (hp : ¬p.Nil) : G.Adj p.penultimate w :=
  by
  conv => rhs; rw [← getVert_length p]
  rw [nil_iff_length_eq] at hp
  convert adj_getVert_succ _ _ <;> omega

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