tsub_tsub_le_tsub_add

Mathlib.Algebra.Order.Sub.Defs

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

← MathLib Explorer

English

c − a − (c − b) ≤ b − a (variant form).

Русский

c − a − (c − b) ≤ b − a (вариант формы).

LaTeX

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

Lean4

theorem tsub_tsub_le_tsub_add {a b c : α} : a - (b - c) ≤ a - b + c :=
  tsub_le_iff_right.2 <|
    calc
      a ≤ a - b + b := le_tsub_add
      _ ≤ a - b + (c + (b - c)) := (add_le_add_left le_add_tsub _)
      _ = a - b + c + (b - c) := (add_assoc _ _ _).symm

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

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

Разделы

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

Аффилиация

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