ofReal_max

Mathlib.Data.ENNReal.Real

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

English

OfReal preserves maxima: ENNReal.ofReal(max(x,y)) = max(ENNReal.ofReal x, ENNReal.ofReal y).

Русский

OfReal сохраняет максимум: ENNReal.ofReal(max(x,y)) = max(ENNReal.ofReal x, ENNReal.ofReal y).

LaTeX

$$$ \operatorname{ofReal}(\max(x,y)) = \max(\operatorname{ofReal}(x), \operatorname{ofReal}(y)) $$$

Lean4

@[simp]
theorem ofReal_max (x y : ℝ) : ENNReal.ofReal (max x y) = max (.ofReal x) (.ofReal y) :=
  ofReal_mono.map_max

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

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

Разделы

Аффилиация

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