set_cons_zero

Mathlib.Data.Seq.Basic

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

English

Setting the first element of a cons changes only the head: (cons hd tl).set 0 hd' = cons hd' tl.

Русский

Установка первого элемента cons меняет только головной элемент: (cons hd tl).set 0 hd' = cons hd' tl.

LaTeX

$$$(cons\ hd\ tl).set\ 0\ hd' = cons\ hd'\ tl$$$

Lean4

@[simp]
theorem set_cons_zero (hd' : α) : (cons hd tl).set 0 hd' = cons hd' tl :=
  update_cons_zero _ _ _

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

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

Разделы

Аффилиация

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