get?_add

Mathlib.Data.WSeq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.WSeq.get?_add

English

For any s, m, n, get? s (m+n) = get? (drop s m) n.

Русский

Для любых s,m,n: get?(s, m+n) = get?(drop(s,m), n).

LaTeX

$$$$\mathrm{get?}(s, m+n) = \mathrm{get?}(\mathrm{drop}(s,m), n).$$$$

Lean4

theorem get?_add (s : WSeq α) (m n) : get? s (m + n) = get? (drop s m) n :=
  congr_arg head (dropn_add _ _ _)

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

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

Разделы

Аффилиация

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