getVert_comp_val_eq_get_support — Mathlib

English

For every walk p, the composition p.getVert ∘ Fin.val equals p.support.get when viewed as functions.

Русский

Для каждого хода p композиция p.getVert ∘ Fin.val равна p.support.get как функции.

LaTeX

$$$ p.\text{getVert} \circ \text{Fin}.\text{val} = p.\text{support}.\text{get} $$$

Lean4

theorem getVert_comp_val_eq_get_support {u v : V} (p : G.Walk u v) : p.getVert ∘ Fin.val = p.support.get := by
  grind [getVert_eq_support_getElem, length_support]

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