neg_lt_of_neg_lt

Mathlib.Data.EReal.Operations

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

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_lt_of_neg_lt {a b : EReal} (h : -a < b) : -b < a :=
  neg_lt_comm.mp h

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

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

Разделы

Аффилиация

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