le_tsub_add_add

Mathlib.Algebra.Order.Sub.Defs

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

English

The same inequality holds: a + b ≤ a − c + (b + c).

Русский

То же неравенство: a + b ≤ a − c + (b + c).

LaTeX

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

Lean4

theorem le_tsub_add_add : a + b ≤ a - c + (b + c) :=
  by
  rw [add_comm a, add_comm (a - c)]
  exact add_le_add_add_tsub

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

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

Разделы

Аффилиация

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