snd_reverse — Mathlib

English

For any walk p, the second vertex of the reversed walk equals the penultimate vertex of p: (p.reverse).snd = p.penultimate.

Русский

Для произвольного хода p в обратном порядке вторая вершина равна предпоследней вершине p: (p.reverse).snd = p.penultimate.

LaTeX

$$$ (p.reverse).\\text{snd} = p.\\text{penultimate} $$$

Lean4

@[simp]
theorem snd_reverse (p : G.Walk u v) : p.reverse.snd = p.penultimate := by simpa using getVert_reverse p 1

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