le_neg_of_le_neg

Mathlib.Data.EReal.Operations

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

English

If a ≤ -b, then -a ≥ b, i.e., b ≤ -a.

Русский

Если a ≤ -b, то -a ≥ b, то есть b ≤ -a.

LaTeX

$$a ≤ -b ⇒ b ≤ -a$$

Lean4

/-- If `a ≤ -b` then `b ≤ -a` on `EReal`. -/
protected theorem le_neg_of_le_neg {a b : EReal} (h : a ≤ -b) : b ≤ -a :=
  EReal.le_neg.mp h

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

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

Разделы

Аффилиация

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