lt_tsub_of_add_lt_right

Mathlib.Algebra.Order.Sub.Defs

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

English

If a + c < b, then a < b − c (under left-cancellative assumptions).

Русский

Если a + c < b, то a < b − c (при левом отменяемом предположении).

LaTeX

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

Lean4

theorem lt_tsub_of_add_lt_right : a + c < b → a < b - c :=
  Contravariant.AddLECancellable.lt_tsub_of_add_lt_right

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

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

Разделы

Аффилиация

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