add_tsub_add_eq_tsub_left — Mathlib

English

Let α be an ordered additive structure with subtraction compatible with the order. Then for all a, b, c in α, a + b - (a + c) = b - c.

Русский

Пусть α является упорядоченной абелевой полугруппой с операцией вычитания, совместимой с порядком. Тогда для любых a, b, c ∈ α выполняется a + b − (a + c) = b − c.

LaTeX

$$$\\forall a,b,c \\in \\alpha\\,\\, a + b - (a + c) = b - c$$$

Lean4

theorem add_tsub_add_eq_tsub_left (a b c : α) : a + b - (a + c) = b - c := by
  rw [add_comm a b, add_comm a c, add_tsub_add_eq_tsub_right]

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