drop — Mathlib

English

Remove the first n elements from a sequence to obtain the tail sequence.

Русский

Удалить первые n элементов последовательности, чтобы получить хвостовую последовательность.

LaTeX

$$$ \mathrm{drop} : \mathrm{Seq}(\alpha) \to \mathbb{N} \to \mathrm{Seq}(\alpha),\quad \mathrm{drop}(s)(0) = s,\quad \mathrm{drop}(s)(n+1) = \mathrm{tail}(\mathrm{drop}(s)(n)).$$$

Lean4

/-- Remove the first `n` elements from the sequence. -/
def drop (s : Seq α) : ℕ → Seq α
  | 0 => s
  | n + 1 => tail (drop s n)

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