sign_neg

Mathlib.Data.Sign.Defs

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

English

If a < 0, then sign a = -1.

Русский

Если a < 0, то sign(a) = -1.

LaTeX

$$$a < 0 \Rightarrow sign(a) = -1$$$

Lean4

@[simp]
theorem sign_neg (ha : a < 0) : sign a = -1 := by rwa [sign_apply, if_neg <| asymm ha, if_pos]

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

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

Разделы

Аффилиация

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