sign_nonpos_iff

Mathlib.Data.Sign.Defs

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

← MathLib Explorer

English

sign a ≤ 0 iff a ≤ 0.

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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