lt_tsub_of_add_lt_left

Mathlib.Algebra.Order.Sub.Defs

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

/-- This lemma (and some of its corollaries) also holds for `ENNReal`, but this proof doesn't work
for it. Maybe we should add this lemma as field to `OrderedSub`? -/
theorem lt_tsub_of_add_lt_left : a + c < b → c < b - a :=
  Contravariant.AddLECancellable.lt_tsub_of_add_lt_left

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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