set_cons_succ

Mathlib.Data.Seq.Basic

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

English

Setting at position n+1 in cons hd tl updates the tail: (cons hd tl).set (n+1) x = cons hd (tl.set n x).

Русский

Установка на позиции n+1 в cons hd tl обновляет хвост: (cons hd tl).set (n+1) x = cons hd (tl.set n x).

LaTeX

$$$(cons\ hd\ tl).set\ (n+1)\ x = cons\ hd\ (tl.set n\ x)$$$

Lean4

@[simp]
theorem set_cons_succ (n : ℕ) : (cons hd tl).set (n + 1) x = cons hd (tl.set n x) :=
  update_cons_succ _ _ _ _

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

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

Разделы

Аффилиация

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