Theorems · Theorem · order theory

eq_tsub_of_add_eq

∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftReflectLE α], a + c = b → a = b - c

Defined in

Mathlib.Algebra.Order.Sub.Defs

Cited by

11 results in Mathlib

Foundations

Depth 12 from the axioms · uses propext

Assumes

PartialOrderAddCommSemigroupSubOrderedSubAddLeftReflectLE