penultimate_cons_of_not_nil — Mathlib

English

Let h be an adjacency, p a nonempty walk; then adding h at the front does not change the penultimate vertex.

Русский

Пусть h — смежность, p — непустой ход; добавление h в начало не изменяет предпоследнюю вершину.

LaTeX

$$$ (cons\, h\, p).penultimate = p.penultimate \\,\\text{ при } h : G.Adj\\ u\\ v\\ and\\ p : G.Walk\\ v\\ w\\, \\text{при } p \\neq Nil $$$

Lean4

theorem penultimate_cons_of_not_nil (h : G.Adj u v) (p : G.Walk v w) (hp : ¬p.Nil) :
    (cons h p).penultimate = p.penultimate :=
  p.notNilRec (by simp) hp h

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