toNNReal_lt_toNNReal — Mathlib

English

For a,b ∈ ENNReal with a,b finite, a.toNNReal < b.toNNReal iff a < b.

Русский

Для конечных a,b ∈ ENNReal имеем a.toNNReal < b.toNNReal тогда и только если a < b.

LaTeX

$$$$ \\forall a,b \\in \\mathbb{R}_{\\ge 0}^{\\infty},\\; a \\neq \\infty \\land b \\neq \\infty \\Rightarrow a^{\\mathrm{toNNReal}} < b^{\\mathrm{toNNReal}} \\iff a < b. $$$$

Lean4

@[simp]
theorem toNNReal_lt_toNNReal (ha : a ≠ ∞) (hb : b ≠ ∞) : a.toNNReal < b.toNNReal ↔ a < b :=
  ⟨fun h => by rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe], toNNReal_strict_mono hb⟩

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