coe_toENNReal_eq_max

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.coe_toENNReal_eq_max

← MathLib Explorer

English

The ENNReal image of x equals max(0, x).

Русский

Изображение x в ENNReal равно max(0, x).

LaTeX

$$$ x.toENNReal = \max(0, x) $$$

Lean4

theorem coe_toENNReal_eq_max {x : EReal} : x.toENNReal = max 0 x :=
  by
  rcases le_total 0 x with (hx | hx)
  · rw [coe_toENNReal hx, max_eq_right hx]
  · rw [toENNReal_of_nonpos hx, max_eq_left hx, coe_ennreal_zero]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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