add_le_of_le_tsub_right_of_le

Mathlib.Algebra.Order.Sub.Unbundled.Basic

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

English

If c is AddLECancellable and c ≤ b, then a + b − c = a + (b − c).

Русский

Если c = AddLECancellable и c ≤ b, тогда a + b − c = a + (b − c).

LaTeX

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

Lean4

theorem add_le_of_le_tsub_right_of_le (h : b ≤ c) (h2 : a ≤ c - b) : a + b ≤ c :=
  (add_le_add_right h2 b).trans_eq <| tsub_add_cancel_of_le h

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

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

Разделы

Аффилиация

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