ofReal_le_ofReal_iff' — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem ofReal_le_ofReal_iff' {p q : ℝ} : ENNReal.ofReal p ≤ .ofReal q ↔ p ≤ q ∨ p ≤ 0 :=
  coe_le_coe.trans Real.toNNReal_le_toNNReal_iff'

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