sign_of_neg

Mathlib.Data.Real.Sign

URI: https://scilib.ai/kg/mathlib#Real.sign_of_neg

English

If r < 0 then sign r = -1.

Русский

Если r < 0, то sign r = -1.

LaTeX

$$$\text{sign}(r) = -1 \quad \text{if } r<0$$$

Lean4

theorem sign_of_neg {r : ℝ} (hr : r < 0) : sign r = -1 := by rw [sign, if_pos hr]

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

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

Разделы

Аффилиация

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