ofReal_min

Mathlib.Data.ENNReal.Real

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

English

OfReal preserves minima: ENNReal.ofReal(min(x,y)) = min(ENNReal.ofReal x, ENNReal.ofReal y).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem ofReal_min (x y : ℝ) : ENNReal.ofReal (min x y) = min (.ofReal x) (.ofReal y) :=
  ofReal_mono.map_min

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

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

Разделы

Аффилиация

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