sign_mul_pos_of_ne_zero

Mathlib.Data.Real.Sign

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

← MathLib Explorer

English

If r ≠ 0, then 0 < sign(r) · r.

Русский

Если r ≠ 0, то 0 < sign(r) · r.

LaTeX

$$$ r \neq 0 \Rightarrow 0 < \text{sign}(r) \cdot r $$$

Lean4

theorem sign_mul_pos_of_ne_zero (r : ℝ) (hr : r ≠ 0) : 0 < sign r * r :=
  by
  refine lt_of_le_of_ne (sign_mul_nonneg r) fun h => hr ?_
  have hs0 := (zero_eq_mul.mp h).resolve_right hr
  exact sign_eq_zero_iff.mp hs0

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

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

Разделы

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

Аффилиация

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