get?_tail

Mathlib.Data.WSeq.Basic

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

English

For any s and n, get? (tail s) n = get? s (n+1).

Русский

Для любых s и n: get?(tail s, n) = get?(s, n+1).

LaTeX

$$$$\mathrm{get?}(\operatorname{tail}(s), n) = \mathrm{get?}(s, n+1).$$$$

Lean4

theorem get?_tail (s : WSeq α) (n) : get? (tail s) n = get? s (n + 1) :=
  congr_arg head (dropn_tail _ _)

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

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

Разделы

Аффилиация

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