add_tsub_le_assoc

Mathlib.Algebra.Order.Sub.Defs

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

← MathLib Explorer

English

For all a,b,c, a + b − c ≤ a + (b − c).

Русский

Для всех a,b,c выполняется a + b − c ≤ a + (b − c).

LaTeX

$$$a + b - c \le a + (b - c)$$$

Lean4

/-- See `add_tsub_assoc_of_le` for the equality. -/
theorem add_tsub_le_assoc : a + b - c ≤ a + (b - c) :=
  by
  rw [tsub_le_iff_left, add_left_comm]
  exact add_le_add_left le_add_tsub a

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

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

Разделы

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

Аффилиация

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