English
The function nnabs is the absolute-value map from ℚ to ℚ≥0.
Русский
Функция nnabs является отображением абсолютного значения из ℚ в ℚ≥0.
LaTeX
$$nnabs : \mathbb{Q} \to \mathbb{Q}_{\ge 0} \,;\; \text{nnabs}(x) = |x| \text{ in codomain } \mathbb{Q}_{\ge 0}.$$
Lean4
/-- The absolute value on `ℚ` as a map to `ℚ≥0`. -/
@[pp_nodot]
def nnabs (x : ℚ) : ℚ≥0 :=
⟨abs x, abs_nonneg x⟩