sub_lt_of_lt_add'

Mathlib.Data.EReal.Operations

URI: https://scilib.ai/kg/mathlib#EReal.sub_lt_of_lt_add'

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$\forall a,b,c \in \mathrm{EReal},\ a < b + c \Rightarrow a - b < c$$$

Lean4

/-- See also `EReal.sub_lt_of_lt_add`. -/
theorem sub_lt_of_lt_add' {a b c : EReal} (h : a < b + c) : a - b < c :=
  sub_lt_of_lt_add <| by rwa [add_comm]

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

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

Разделы

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

Аффилиация

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