dropn_add — Mathlib

English

Let s be a sequence. For all natural numbers m and n, dropping the first m + n elements of s yields the same sequence as first dropping m elements and then dropping n more elements.

Русский

Пусть имеется последовательность s. Для любых натуральных чисел m и n удаление первых m + n элементов приводит к той же последовательности, что и первое удаление m элементов, а затем еще n элементов.

LaTeX

$$$$ \\mathrm{drop}_{m+n}(s) = \\mathrm{drop}_{n}(\\mathrm{drop}_{m}(s)). $$$$

Lean4

theorem dropn_add (s : Seq α) (m) : ∀ n, drop s (m + n) = drop (drop s m) n
  | 0 => rfl
  | n + 1 => congr_arg tail (dropn_add s _ n)

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