getVert — Mathlib

English

Get the nth vertex along a walk; if n is out of range, return the end vertex.

Русский

Извлечь n-ую вершину траектории; если n вне диапазона, вернуть конечную вершину.

LaTeX

$$def getVert {u v : V} : G.Walk u v → ℕ → V$$

Lean4

/-- Get the `n`th vertex from a walk, where `n` is generally expected to be
between `0` and `p.length`, inclusive.
If `n` is greater than or equal to `p.length`, the result is the path's endpoint. -/
def getVert {u v : V} : G.Walk u v → ℕ → V
  | nil, _ => u
  | cons _ _, 0 => u
  | cons _ q, n + 1 => q.getVert n

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