toReal_mono — Mathlib

English

Let a and b be elements of ENNReal with b finite (b ≠ ∞) and a ≤ b. Then their real realizations satisfy toReal(a) ≤ toReal(b).

Русский

Пусть a и b принадлежат ENNReal и b конечен (b ≠ ∞), а также a ≤ b. Тогда их образы в действительных числах удовлетворяют toReal(a) ≤ toReal(b).

LaTeX

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

Lean4

@[gcongr]
theorem toReal_mono (hb : b ≠ ∞) (h : a ≤ b) : a.toReal ≤ b.toReal :=
  (toReal_le_toReal (ne_top_of_le_ne_top hb h) hb).2 h

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