toReal_ofReal'

Mathlib.Data.ENNReal.Basic

URI: https://scilib.ai/kg/mathlib#ENNReal.toReal_ofReal'

English

For any real r, (ENNReal.ofReal r).toReal = max r 0.

Русский

Для любого действительного r, (ENNReal.ofReal r).toReal = max r 0.

LaTeX

$$$ (\operatorname{ofReal} r).toReal = \max(r,0) $$$

Lean4

theorem toReal_ofReal' {r : ℝ} : (ENNReal.ofReal r).toReal = max r 0 :=
  rfl

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

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

Разделы

Аффилиация

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