toReal_le_toReal — Mathlib

English

If a,b ∈ ENNReal with a ≠ ∞ and b ≠ ∞, then a.toReal ≤ b.toReal iff a ≤ b.

Русский

Пусть a,b ∈ ENNReal, a ≠ ∞ и b ≠ ∞. Тогда a.toReal ≤ b.toReal эквивалентно a ≤ b.

LaTeX

$$$(a \\neq \\infty) \\land (b \\neq \\infty) \\Rightarrow a^{\\mathrm{toReal}} \\le b^{\\mathrm{toReal}} \\iff a \\le b$$$

Lean4

@[simp]
theorem toReal_le_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

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