add_tsub_assoc_of_le

Mathlib.Algebra.Order.Sub.Unbundled.Basic

URI: https://scilib.ai/kg/mathlib#AddLECancellable.add_tsub_assoc_of_le

← MathLib Explorer

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

protected theorem add_tsub_assoc_of_le (hc : AddLECancellable c) (h : c ≤ b) (a : α) : a + b - c = a + (b - c) := by
  conv_lhs => rw [← add_tsub_cancel_of_le h, add_comm c, ← add_assoc, hc.add_tsub_cancel_right]

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

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

Разделы

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

Аффилиация

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