getVert_eq_support_getElem — Mathlib

English

For a walk p and n ≤ length(p), the nth vertex along the walk equals the nth element of the support list.

Русский

Для хода p и n ≤ длины(p) n-ая вершина вдоль хода совпадает с n-ым элементом списка поддержки.

LaTeX

$$$ p.\text{getVert}(n) = p.\text{support}[n] \quad \text{для } n \le p.\text{length} $$$

Lean4

theorem getVert_eq_support_getElem {u v : V} {n : ℕ} (p : G.Walk u v) (h : n ≤ p.length) :
    p.getVert n = p.support[n]'(p.length_support ▸ Nat.lt_add_one_of_le h) := by
  cases p with
  | nil => simp
  | cons =>
    cases n with
    | zero => simp
    | succ n =>
      simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]
      exact getVert_eq_support_getElem _ (Nat.sub_le_of_le_add h)

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