getLast_darts_snd — Mathlib

English

The last coordinate of the last dart equals the ending vertex of the walk, provided the list of darts is nonempty.

Русский

Последняя координата последнего дротика равна конечной вершине обхода, если список дротиков не пуст.

LaTeX

$$$\text{(p.\\darts.\\getLast hp).\\snd} = b$$$

Lean4

@[simp]
theorem getLast_darts_snd {G : SimpleGraph V} {a b : V} (p : G.Walk a b) (hp : p.darts ≠ []) :
    (p.darts.getLast hp).snd = b :=
  by
  rw [← List.getLast_map (f := fun x : G.Dart ↦ x.snd)]
  · simp_rw [p.map_snd_darts, List.getLast_tail, p.getLast_support]
  · simpa

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