add_tsub_add_le_tsub_right

Mathlib.Algebra.Order.Sub.Defs

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

← MathLib Explorer

English

a + c − (b + c) ≤ a − b.

Русский

a + c − (b + c) ≤ a − b.

LaTeX

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

Lean4

/-- See `add_tsub_add_eq_tsub_right` for the equality. -/
theorem add_tsub_add_le_tsub_right : a + c - (b + c) ≤ a - b :=
  by
  rw [tsub_le_iff_left, add_right_comm]
  exact add_le_add_right le_add_tsub c

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

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

Разделы

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

Аффилиация

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