neg_le_of_neg_le

Mathlib.Data.EReal.Operations

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

English

If -a ≤ b, then -b ≤ a on EReal.

Русский

Если -a ≤ b, то -b ≤ a на EReal.

LaTeX

$$(-a ≤ b) ⇒ (-b ≤ a)$$

Lean4

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

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

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

Разделы

Аффилиация

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