update_cons_succ

Mathlib.Data.Seq.Basic

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.update_cons_succ

English

Updating at position n+1 in cons hd tl yields cons hd (tl.update n f).

Русский

Обновление на позиции n+1 в cons hd tl даёт cons hd – tl.update n f.

LaTeX

$$$(cons\ hd\ tl).update\ (n+1)\ f = cons\ hd\ (tl.update\ n\ f)$$$

Lean4

@[simp]
theorem update_cons_succ (n : ℕ) : (cons hd tl).update (n + 1) f = cons hd (tl.update n f) :=
  by
  ext1 n
  cases n <;> simp [get?_update]

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

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

Разделы

Аффилиация

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