drop — Mathlib

English

Dropping the first n elements yields a stream whose i-th element equals the (i+n)-th element of the original stream.

Русский

Пропуск первых n элементов порождает поток, в котором i-й элемент равен (i+n)-му элементу исходного потока.

LaTeX

$$$ \forall n \in \mathbb{N},\ \forall s:\text{Stream}'(\alpha),\ \forall i:\mathbb{N},\ (\text{drop}(n,s))(i) = s(i+n). $$$

Lean4

/-- Drop first `n` elements of a stream. -/
def drop (n : ℕ) (s : Stream' α) : Stream' α := fun i => s.get (i + n)

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