ofReal_le_ofReal — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[gcongr, bound]
theorem ofReal_le_ofReal {p q : ℝ} (h : p ≤ q) : ENNReal.ofReal p ≤ ENNReal.ofReal q := by
  simp [ENNReal.ofReal, Real.toNNReal_le_toNNReal h]

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