toReal_eq_toReal — Mathlib

English

For finite ENNReal a,b (a ≠ ∞, b ≠ ∞), a.toReal = b.toReal ↔ a = b.

Русский

Для конечных a,b ∈ ENNReal (a,b ≠ ∞) выполняется a.toReal = b.toReal ↔ a = b.

LaTeX

$$$a \neq \infty,\; b \neq \infty \Rightarrow a.toReal = b.toReal \iff a = b$$$

Lean4

theorem toReal_eq_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal = b.toReal ↔ a = b :=
  by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  simp only [coe_inj, NNReal.coe_inj, coe_toReal]

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