sign_mul_nonneg

Mathlib.Data.Real.Sign

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

← MathLib Explorer

English

For any real r, 0 ≤ sign(r) · r.

Русский

Для любого r ∈ ℝ выполняется 0 ≤ sign(r) · r.

LaTeX

$$$0 \leq \text{sign}(r) \cdot r$$$

Lean4

theorem sign_mul_nonneg (r : ℝ) : 0 ≤ sign r * r :=
  by
  obtain hn | rfl | hp := lt_trichotomy r (0 : ℝ)
  · rw [sign_of_neg hn]
    exact mul_nonneg_of_nonpos_of_nonpos (by simp) hn.le
  · rw [mul_zero]
  · rw [sign_of_pos hp, one_mul]
    exact hp.le

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

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

Разделы

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

Аффилиация

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