sub_le_of_le_add'

Mathlib.Data.EReal.Operations

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

/-- See also `EReal.sub_le_of_le_add`. -/
theorem sub_le_of_le_add' {a b c : EReal} (h : a ≤ b + c) : a - b ≤ c :=
  sub_le_of_le_add (add_comm b c ▸ h)

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

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

Разделы

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

Аффилиация

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