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⟩