English
Let r and q be nonnegative real numbers. The natural embedding of NNReal into ENNReal preserves and reflects order: (↑r) < (↑q) in ENNReal if and only if r < q in NNReal.
Русский
Пусть r и q — неотрицательные действительные числа. Естественное вложение NNReal в ENNReal сохраняет и отражает порядок: (↑r) < (↑q) в ENNReal тогда и только тогда, когда r < q в NNReal.
LaTeX
$$$ (\uparrow r : \mathbb{R}_{\ge 0}^{\infty}) < \uparrow q \iff r < q $$$
Lean4
@[simp, norm_cast]
theorem coe_lt_coe : (↑r : ℝ≥0∞) < ↑q ↔ r < q :=
WithTop.coe_lt_coe