getOrElse_of_not_dom

Mathlib.Data.Part

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

English

If a is not defined, getOrElse a d = d.

Русский

Если a не определено, то getOrElse a d = d.

LaTeX

$$$ \forall a : \mathrm{Part}(\alpha), \neg a.\\Dom \rightarrow \forall d : \alpha, \\operatorname{getOrElse}(a,d) = d $$$

Lean4

theorem getOrElse_of_not_dom (a : Part α) (h : ¬a.Dom) [Decidable a.Dom] (d : α) : getOrElse a d = d :=
  dif_neg h

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

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

Разделы

Аффилиация

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