sign_neg

Mathlib.Data.Real.Sign

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

← MathLib Explorer

English

sign(-r) = - sign(r) for all real r.

Русский

sign(-r) = -sign(r) для всех r ∈ ℝ.

LaTeX

$$$ \text{sign}(-r) = -\text{sign}(r) $$$

Lean4

theorem sign_neg {r : ℝ} : sign (-r) = -sign r :=
  by
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn, sign_of_pos (neg_pos.mpr hn), neg_neg]
  · rw [sign_zero, neg_zero, sign_zero]
  · rw [sign_of_pos hp, sign_of_neg (neg_lt_zero.mpr hp)]

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

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

Разделы

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

Аффилиация

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