English
There is a canonical embedding of real numbers into NNReal, given by r ↦ ⟨max(r,0), proof⟩; this maps negative numbers to 0 and keeps nonnegative numbers unchanged.
Русский
Существует каноническое вложение действительных чисел в NNReal, заданное отображением r ↦ ⟨max(r,0), доказательство⟩; отрицательные числа переходят в 0, неотрицательные сохраняются без изменений.
LaTeX
$$$ \mathsf{Real.toNNReal}(r) = \langle \max(r,0), 0 \le \max(r,0) \rangle $$$
Lean4
/-- Reinterpret a real number `r` as a non-negative real number. Returns `0` if `r < 0`. -/
def _root_.Real.toNNReal (r : ℝ) : ℝ≥0 :=
⟨max r 0, le_max_right _ _⟩
