sign — Mathlib

English

The sign function maps negative numbers to -1, positive numbers to 1, and zero to 0.

Русский

Функция знака отображает отрицательные числа в -1, положительные — в 1, ноль — в 0.

LaTeX

$$$\operatorname{sign}(r) = \begin{cases}-1,& r<0,\\ 0,& r=0,\\ 1,& r>0.\end{cases}$$$

Lean4

/-- The sign function that maps negative real numbers to -1, positive numbers to 1, and 0
otherwise. -/
noncomputable def sign (r : ℝ) : ℝ :=
  if r < 0 then -1 else if 0 < r then 1 else 0

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