toReal_ofReal

Mathlib.Data.ENNReal.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem toReal_ofReal {r : ℝ} (h : 0 ≤ r) : (ENNReal.ofReal r).toReal = r :=
  max_eq_left h

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

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

Разделы

Аффилиация

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