sub_lt_of_lt_add

Mathlib.Data.ENNReal.Operations

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

English

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

Русский

Если c ≤ a и a < b + c, то a − c < b.

LaTeX

$$$$ c \le a \land a < b + c \Rightarrow a - c < b. $$$$

Lean4

protected theorem sub_lt_of_lt_add (hac : c ≤ a) (h : a < b + c) : a - c < b :=
  ((cancel_of_lt' <| hac.trans_lt h).tsub_lt_iff_right hac).mpr h

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

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

Разделы

Аффилиация

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