productive_dropn — Mathlib

English

Dropping the first n elements preserves productivity: if s is productive, then drop s n is productive.

Русский

Обрезание первых n элементов сохраняет продуктивность: если s продуктивна, то drop s n продуктивна.

LaTeX

$$$$ (\mathrm{drop}\ s\ n).\mathrm{Productive}. $$$$

Lean4

instance productive_dropn (s : WSeq α) [Productive s] (n) : Productive (drop s n) :=
  ⟨fun m => by rw [← get?_add]; infer_instance⟩

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