ofReal_eq_ofReal_iff — Mathlib

English

For p,q ∈ ℝ with p,q ≥ 0, ENNReal.ofReal p = ENNReal.ofReal q iff p = q.

Русский

Для p,q ∈ ℝ с p,q ≥ 0, ENNReal.ofReal p = ENNReal.ofReal q эквивалентно p = q.

LaTeX

$$$$ \\forall p,q \\in \\mathbb{R}_{\\ge 0},\\; \\operatorname{ofReal}(p) = \\operatorname{ofReal}(q) \\iff p = q. $$$$

Lean4

@[simp]
theorem ofReal_eq_ofReal_iff {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) : ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]

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