getI_nil

Mathlib.Data.List.GetD

URI: https://scilib.ai/kg/mathlib#List.getI_nil

English

The equality with getElem? reduces to getD for either the in-range case or the default case.

Русский

Равенство через getElem? сводится к getD в случаях попадания в диапазон или по умолчанию.

LaTeX

$$$$ l.getD n d = (l[n]?.getD d) $$$$

Lean4

@[simp]
theorem getI_nil : getI ([] : List α) n = default :=
  rfl

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

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

Разделы

Аффилиация

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