nnabs

Mathlib.Data.NNRat.Defs

URI: https://scilib.ai/kg/mathlib#Rat.nnabs

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⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru