tsub_add_tsub_comm

Mathlib.Algebra.Order.Sub.Unbundled.Basic

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

← MathLib Explorer

English

If b − a is cancellable and a ≤ b, then b − (b − a) = a.

Русский

Если b − a канцелируемо и a ≤ b, тогда b − (b − a) = a.

LaTeX

$$$ \forall a,b \in \alpha,\; AddLECancellable(b - a) \land a \le b \Rightarrow b - (b - a) = a $$$

Lean4

theorem tsub_add_tsub_comm (hba : b ≤ a) (hdc : d ≤ c) : a - b + (c - d) = a + c - (b + d) :=
  Contravariant.AddLECancellable.tsub_add_tsub_comm Contravariant.AddLECancellable hba hdc

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

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

Разделы

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

Аффилиация

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