sign_neg

Mathlib.Data.Sign.Defs

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

← MathLib Explorer

English

In a additive group with left-strict monotone map, sign(-a) = -sign(a).

Русский

В аддитивной группе с лево-строго монотонной картой, sign(-a) = -sign(a).

LaTeX

$$sign(-a) = -sign(a)$$

Lean4

theorem sign_neg [AddLeftStrictMono α] (a : α) : sign (-a) = -sign a :=
  by
  simp_rw [sign_apply, Left.neg_pos_iff, Left.neg_neg_iff]
  split_ifs with h h'
  · exact False.elim (lt_asymm h h')
  · simp
  · simp
  · simp

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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