toReal_eq_toReal_iff' — Mathlib

English

For x, y in ENNReal with x ≠ ∞ and y ≠ ∞, x.toReal = y.toReal iff x = y.

Русский

Для x, y в ENNReal при условии x ≠ ∞ и y ≠ ∞, x.toReal = y.toReal тогда и только тогда, когда x = y.

LaTeX

$$$ x \neq \infty \land y \neq \infty \Rightarrow x.toReal = y.toReal \iff x = y $$$

Lean4

theorem toReal_eq_toReal_iff' {x y : ℝ≥0∞} (hx : x ≠ ⊤) (hy : y ≠ ⊤) : x.toReal = y.toReal ↔ x = y := by
  simp only [ENNReal.toReal, NNReal.coe_inj, toNNReal_eq_toNNReal_iff' hx hy]

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