ofReal_le_ofReal_iff — Mathlib

English

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

Русский

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

LaTeX

$$$$ \\forall p,q \\in \\mathbb{R},\\; q \\ge 0 \\Rightarrow ENNReal.ofReal(p) \\le ENNReal.ofReal(q) \\iff p \\le q. $$$$

Lean4

@[simp]
theorem ofReal_le_ofReal_iff {p q : ℝ} (h : 0 ≤ q) : ENNReal.ofReal p ≤ ENNReal.ofReal q ↔ p ≤ q := by
  rw [ENNReal.ofReal, ENNReal.ofReal, coe_le_coe, Real.toNNReal_le_toNNReal_iff h]

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