getVert_eq_getD_support — Mathlib

English

For any walk p and any n, p.getVert(n) equals p.support.getD(n, v) where v is the default vertex.

Русский

Для движения p и любого n вершина p.getVert(n) равна p.support.getD(n, v) (значение по умолчанию v).

LaTeX

$$$ p.\text{getVert}(n) = p.\text{support}.\text{getD}(n, v) $$$

Lean4

theorem getVert_eq_getD_support {u v : V} (p : G.Walk u v) (n : ℕ) : p.getVert n = p.support.getD n v :=
  by
  by_cases h : n ≤ p.length
  · simp [← getVert_eq_support_getElem? p h]
  grind [getVert_of_length_le, length_support]

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