toReal_ofReal_eq_iff

Mathlib.Data.ENNReal.Basic

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

← MathLib Explorer

English

For any real a, (ENNReal.ofReal a).toReal = a if and only if a ≥ 0.

Русский

Для любого действительного a, (ENNReal.ofReal a).toReal = a тогда и только тогда, когда a ≥ 0.

LaTeX

$$$$ (ENNReal.ofReal a).toReal = a \iff 0 \le a. $$$$

Lean4

@[simp]
theorem toReal_ofReal_eq_iff {a : ℝ} : (ENNReal.ofReal a).toReal = a ↔ 0 ≤ a :=
  ⟨fun h => by
    rw [← h]
    exact toReal_nonneg, toReal_ofReal⟩

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

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

Разделы

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

Аффилиация

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