toReal_toENNReal

Mathlib.Data.EReal.Basic

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

← MathLib Explorer

English

If x ≥ 0 then x.toENNReal.toReal = x.toReal.

Русский

Если x ≥ 0, то x.toENNReal.toReal = x.toReal.

LaTeX

$$$ 0 \le x \Rightarrow x.toENNReal.toReal = x.toReal $$$

Lean4

@[simp]
theorem toReal_toENNReal {x : EReal} (hx : 0 ≤ x) : x.toENNReal.toReal = x.toReal :=
  by
  by_cases h : x = ⊤
  · simp [h]
  · simp [h, toReal_nonneg hx]

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

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

Разделы

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

Аффилиация

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