lt_add_of_tsub_lt_right

Mathlib.Algebra.Order.Sub.Defs

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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