toReal_lt_toReal — Mathlib

English

For a,b ∈ ENNReal with a,b finite (a ≠ ∞ and b ≠ ∞), we have toReal(a) < toReal(b) if and only if a < b.

Русский

Пусть a,b принадлежат ENNReal и конечны; тогда toReal(a) < toReal(b) тогда и только если a < b.

LaTeX

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

Lean4

@[simp]
theorem toReal_lt_toReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toReal < b.toReal ↔ a < b :=
  by
  lift a to ℝ≥0 using ha
  lift b to ℝ≥0 using hb
  norm_cast

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