getOrElse_none

Mathlib.Data.Part

URI: https://scilib.ai/kg/mathlib#Part.getOrElse_none

English

For any d, getOrElse none d = d.

Русский

Для любого d, getOrElse none d = d.

LaTeX

$$$ \forall d : \alpha, \\operatorname{getOrElse}(\\mathrm{none}, d) = d $$$

Lean4

@[simp]
theorem getOrElse_none (d : α) [Decidable (none : Part α).Dom] : getOrElse none d = d :=
  none.getOrElse_of_not_dom not_none_dom d

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

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

Разделы

Аффилиация

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