getVert_append — Mathlib

English

The i-th vertex of the concatenation p.concat q is p.getVert i if i < p.length, otherwise q.getVert(i - p.length).

Русский

i-я вершина конкатенации p.concat q равна p.getVert i, если i < |p|, иначе равна q.getVert(i - |p|).

LaTeX

$$$(p.concat(q)).getVert(i) = \begin{cases} p.getVert(i), & i < p.length, \\ q.getVert(i - p.length), & \text{else} \end{cases}$$$

Lean4

theorem getVert_append {u v w : V} (p : G.Walk u v) (q : G.Walk v w) (i : ℕ) :
    (p.append q).getVert i = if i < p.length then p.getVert i else q.getVert (i - p.length) := by
  induction p generalizing i with
  | nil => simp
  | cons h p ih => cases i <;> simp [getVert, ih, Nat.succ_lt_succ_iff]

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