drop — Mathlib

English

The walk obtained by removing the first n darts of a walk p is denoted p.drop n.

Русский

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

LaTeX

$$$ \text{drop}(p,n) extrm{ is the walk obtained by removing the first } n \text{ darts of } p. $$$

Lean4

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

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