toReal_mono' — Mathlib

English

Let a,b ∈ ENNReal with a ≤ b and (b = ∞ → a = ∞). Then a.toReal ≤ b.toReal.

Русский

Пусть a,b ∈ ENNReal, выполнено a ≤ b и (b = ∞ → a = ∞). Тогда a.toReal ≤ b.toReal.

LaTeX

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

Lean4

theorem toReal_mono' (h : a ≤ b) (ht : b = ∞ → a = ∞) : a.toReal ≤ b.toReal :=
  by
  rcases eq_or_ne a ∞ with rfl | ha
  · exact toReal_nonneg
  · exact toReal_mono (mt ht ha) h

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