tsub_add_eq_tsub_tsub

Mathlib.Algebra.Order.Sub.Defs

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

English

a − (b + c) = a − b − c.

Русский

a − (b + c) = a − b − c.

LaTeX

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

Lean4

theorem tsub_add_eq_tsub_tsub (a b c : α) : a - (b + c) = a - b - c :=
  (tsub_tsub _ _ _).symm

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

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

Разделы

Аффилиация

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