update_nil

Mathlib.Data.Seq.Basic

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

English

Updating the empty sequence by any index leaves it unchanged: update nil n f = nil.

Русский

Обновление пустой последовательности по любому индексу не меняет её: update nil n f = nil.

LaTeX

$$$update\ nil\ n\ f = nil$$$

Lean4

@[simp]
theorem update_nil (n : ℕ) : update nil n f = nil := by
  ext1 m
  simp [get?_update]

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

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

Разделы

Аффилиация

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