sign_apply_eq_of_ne_zero

Mathlib.Data.Real.Sign

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

← MathLib Explorer

English

If r ≠ 0, then sign r ∈ { -1, 1 }.

Русский

Если r ≠ 0, то sign r ∈ { -1, 1 }.

LaTeX

$$$ r \neq 0 \Rightarrow (\text{sign}(r) = -1 \lor \text{sign}(r) = 1) $$$

Lean4

/-- This lemma is useful for working with `ℝˣ` -/
theorem sign_apply_eq_of_ne_zero (r : ℝ) (h : r ≠ 0) : sign r = -1 ∨ sign r = 1 :=
  h.lt_or_gt.imp sign_of_neg sign_of_pos

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

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

Разделы

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

Аффилиация

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