take — Mathlib

English

The walk taken by taking the first n darts of p is defined recursively by take.

Русский

Ход take(p,n) задаётся рекурсивно как ход, получаемый взятием первых n дротиков хода p.

LaTeX

$$$ \text{take} : G.Walk u v \times \mathbb{N} \to G.Walk u (p.getVert n) $$$

Lean4

/-- The walk obtained by taking the first `n` darts of a walk. -/
def take {u v : V} (p : G.Walk u v) (n : ℕ) : G.Walk u (p.getVert n) :=
  match p, n with
  | .nil, _ => .nil
  | p, 0 => nil.copy rfl (getVert_zero p).symm
  | .cons h q, (n + 1) => .cons h (q.take n)

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