ofReal_le_of_le_toReal — Mathlib

English

If a ≤ toReal(b) for a ∈ ℝ and b ∈ ENNReal, then ofReal(a) ≤ b.

Русский

Если a ≤ toReal(b) для a ∈ ℝ и b ∈ ENNReal, то ofReal(a) ≤ b.

LaTeX

$$$$ \\forall a \\in \\mathbb{R},\\; \\forall b \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; a \\le \\operatorname{toReal}(b) \\Rightarrow \\operatorname{ofReal}(a) \\le b. $$$$

Lean4

theorem ofReal_le_of_le_toReal {a : ℝ} {b : ℝ≥0∞} (h : a ≤ ENNReal.toReal b) : ENNReal.ofReal a ≤ b :=
  (ofReal_le_ofReal h).trans ofReal_toReal_le

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