toReal_eq_zero_iff — Mathlib

English

For any ENNReal x, its real value is zero exactly when x is 0 or ∞.

Русский

Для любого ENNReal x его вещественное значение равно нулю тогда и только тогда, когда x равно 0 или ∞.

LaTeX

$$$$ x.toReal = 0 \\Longleftrightarrow \\ x = 0 \,\lor\, x = \infty. $$$$

Lean4

theorem toReal_eq_zero_iff (x : ℝ≥0∞) : x.toReal = 0 ↔ x = 0 ∨ x = ∞ := by simp [ENNReal.toReal, toNNReal_eq_zero_iff]

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