map_fst_darts — Mathlib

English

The map of the first coordinates of p.darts equals the walk's support without its last element.

Русский

Отображение первых координат дротиков обхода равно опоре обхода без последнего элемента.

LaTeX

$$$p.\\darts.\\map\\ (fun x \\to x.\\fst) = p.\\support.\\dropLast$$$

Lean4

theorem map_fst_darts {u v : V} (p : G.Walk u v) : p.darts.map (·.fst) = p.support.dropLast := by
  simpa! using congr_arg List.dropLast (map_fst_darts_append p)

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