Theorems · Theorem · order theory

AddLECancellable.tsub_tsub_cancel_of_le

∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b : α}, AddLECancellable (b - a) → a ≤ b → b - (b - a) = a

Defined in

Mathlib.Algebra.Order.Sub.Unbundled.Basic

Cited by

4 results in Mathlib

Foundations

Depth 11 from the axioms · uses propext, Quot.sound

Assumes

AddCommSemigroupPartialOrderExistsAddOfLEAddLeftMonoSubOrderedSub