toReal_le_of_le_ofReal — Mathlib

English

If hb: 0 ≤ b and a ≤ ENNReal.ofReal(b), then ENNReal.toReal(a) ≤ b. In other words, real-to-ENNReal comparison reflects back to the real scale for finite ENNReal numbers.

Русский

Если hb: 0 ≤ b и a ≤ ENNReal.ofReal(b), тогда ENNReal.toReal(a) ≤ b. Иначе говоря, сравнение в REAL отражается обратно для конечных чисел ENNReal.

LaTeX

$$$0 \le b \Rightarrow a \le \operatorname{ofReal}(b) \Rightarrow \operatorname{toReal}(a) \le b \,.$$

Lean4

theorem toReal_le_of_le_ofReal {a : ℝ≥0∞} {b : ℝ} (hb : 0 ≤ b) (h : a ≤ ENNReal.ofReal b) : ENNReal.toReal a ≤ b :=
  have ha : a ≠ ∞ := ne_top_of_le_ne_top ofReal_ne_top h
  (le_ofReal_iff_toReal_le ha hb).1 h

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