neg_le_zero

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.neg_le_zero

English

For every a ∈ EReal, -a ≤ 0 if and only if 0 ≤ a.

Русский

Для любого a ∈ EReal верно: -a ≤ 0 эквивалентно 0 ≤ a.

LaTeX

$$$-a \le 0 \iff 0 \le a$$$

Lean4

@[simp]
protected theorem neg_le_zero {a : EReal} : -a ≤ 0 ↔ 0 ≤ a := by rw [EReal.neg_le, neg_zero]

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

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

Разделы

Аффилиация

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