sign_zero

Mathlib.Data.Sign.Defs

URI: https://scilib.ai/kg/mathlib#sign_zero

English

sign a equals the piecewise value 1 if a > 0, -1 if a < 0, and 0 otherwise.

Русский

sign a равно 1, если a > 0, равно -1, если a < 0, иначе 0.

LaTeX

$$$sign(a) = \begin{cases}1 & 0 < a \\ -1 & a < 0 \\ 0 & \text{ иначе} \end{cases}$$$

Lean4

@[simp]
theorem sign_zero : sign (0 : α) = 0 := by simp [sign_apply]

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

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

Разделы

Аффилиация

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