getElem?_getD_singleton_default_eq

Mathlib.Data.List.GetD

URI: https://scilib.ai/kg/mathlib#List.getElem?_getD_singleton_default_eq

English

For the singleton list [d], the n-th element is d if it exists, and getD of that element equals d.

Русский

Для одноэлементного списка [d] n-й элемент равен d если он существует, и getD от этого элемента равен d.

LaTeX

$$$$ [d][n]?.getD d = d $$$$

Lean4

@[simp]
theorem getElem?_getD_singleton_default_eq (n : ℕ) : [d][n]?.getD d = d := by cases n <;> simp

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

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

Разделы

Аффилиация

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