toReal_eq_toReal_iff — Mathlib

English

For x, y in ENNReal, x.toReal = y.toReal iff x = y or x = 0 ∧ y = ∞ or x = ∞ ∧ y = 0.

Русский

Для x, y в ENNReal, x.toReal = y.toReal тогда и только тогда, когда x = y или x = 0 и y = ∞ или x = ∞ и y = 0.

LaTeX

$$$ x.toReal = y.toReal \iff x = y \lor x = 0 \land y = \top \lor x = \top \land y = 0 $$$

Lean4

theorem toReal_eq_toReal_iff (x y : ℝ≥0∞) : x.toReal = y.toReal ↔ x = y ∨ x = 0 ∧ y = ⊤ ∨ x = ⊤ ∧ y = 0 := by
  simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff]

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