tsub_tsub

Mathlib.Algebra.Order.Sub.Defs

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

← MathLib Explorer

English

For all b,a,c, b − a − c = b − (a + c).

Русский

Для всех b,a,c выполняется b − a − c = b − (a + c).

LaTeX

$$$b - a - c = b - (a + c)$$$

Lean4

theorem tsub_tsub (b a c : α) : b - a - c = b - (a + c) :=
  by
  apply le_antisymm
  · rw [tsub_le_iff_left, tsub_le_iff_left, ← add_assoc, ← tsub_le_iff_left]
  · rw [tsub_le_iff_left, add_assoc, ← tsub_le_iff_left, ← tsub_le_iff_left]

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

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

Разделы

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

Аффилиация

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