getOrElse_of_dom

Mathlib.Data.Part

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

English

Let a ∈ Part α with a.Dom, then getOrElse a d = a.get h for h : a.Dom.

Русский

Пусть a ∈ Part α и a.Dom; тогда getOrElse a d = a.get h для некоторого h : a.Dom.

LaTeX

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

Lean4

theorem getOrElse_of_dom (a : Part α) (h : a.Dom) [Decidable a.Dom] (d : α) : getOrElse a d = a.get h :=
  dif_pos h

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

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

Разделы

Аффилиация

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