get?_nil

Mathlib.Data.Seq.Defs

URI: https://scilib.ai/kg/mathlib#Stream'.Seq.get?_nil

English

The nth element of the empty sequence is none for every n.

Русский

n-й элемент пустой последовательности равен none для всех n.

LaTeX

$$$\\forall n:\\mathbb{N},\\; (@\\,\\text{nil} \\;\\alpha).\\mathrm{get?}\\,n = \\mathrm{none}$$$

Lean4

@[simp]
theorem get?_nil (n : ℕ) : (@nil α).get? n = none :=
  rfl

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

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

Разделы

Аффилиация

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