sign_nonneg_iff

Mathlib.Data.Sign.Defs

URI: https://scilib.ai/kg/mathlib#sign_nonneg_iff

← MathLib Explorer

English

0 ≤ sign a iff 0 ≤ a.

Русский

0 ≤ sign(a) тогда и только тогда, когда 0 ≤ a.

LaTeX

$$0 \le sign(a) \iff 0 \le a$$

Lean4

@[simp]
theorem sign_nonneg_iff : 0 ≤ sign a ↔ 0 ≤ a :=
  by
  rcases lt_trichotomy 0 a with (h | h | h)
  · simp [h, h.le]
  · simp [← h]
  · simp [h, h.not_ge]

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

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

Разделы

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

Аффилиация

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