dropn_tail — Mathlib

English

Let s be a sequence and n a natural number. Dropping n elements from the tail of s is the same as dropping n + 1 elements from s.

Русский

Пусть имеется последовательность s и натуральное число n. Удаление n элементов из хвоста s эквивалентно удалению n + 1 элементов из s.

LaTeX

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

Lean4

theorem dropn_tail (s : Seq α) (n) : drop (tail s) n = drop s (n + 1) := by rw [Nat.add_comm]; symm; apply dropn_add

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