lt_add_of_tsub_lt_left

Mathlib.Algebra.Order.Sub.Defs

URI: https://scilib.ai/kg/mathlib#lt_add_of_tsub_lt_left

English

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

Русский

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

LaTeX

$$$ a - b < c \Rightarrow a < b + c $$$

Lean4

theorem lt_add_of_tsub_lt_left (h : a - b < c) : a < b + c :=
  Contravariant.AddLECancellable.lt_add_of_tsub_lt_left h

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

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

Разделы

Аффилиация

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