tsub_add_eq_tsub_tsub_swap — Mathlib

English

Let a, b, c be elements of an ordered additive semigroup with subtraction. Then a − (b + c) = (a − c) − b.

Русский

Пусть a, b, c — элементы упорядоченного аддитивного полугруппы с вычитанием. Тогда a − (b + c) = (a − c) − b.

LaTeX

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

Lean4

theorem tsub_add_eq_tsub_tsub_swap (a b c : α) : a - (b + c) = a - c - b :=
  by
  rw [add_comm]
  apply tsub_add_eq_tsub_tsub

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