dropn_add

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.dropn_add

English

For any s,m,n, dropping m+n from s equals dropping n from the result of dropping m.

Русский

Пусть s : WSeq α, m,n : Nat. drop(s, m+n) = drop(drop(s,m), n).

LaTeX

$$$$\operatorname{drop}(s, m+n) = \operatorname{drop}(\operatorname{drop}(s,m), n).$$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru