sub_lt_of_lt_add

Mathlib.Data.EReal.Operations

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

English

If a < b + c, then a − c < b.

Русский

Если a < b + c, então a − c < b.

LaTeX

$$$\forall a,b,c \in \mathrm{EReal},\ a < b + c \Rightarrow a - c < b$$$

Lean4

theorem sub_lt_of_lt_add {a b c : EReal} (h : a < b + c) : a - c < b :=
  add_lt_of_lt_sub <| by rwa [sub_eq_add_neg, neg_neg]

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

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

Разделы

Аффилиация

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