coe_lt_coe — Mathlib

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

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