Theorems · Theorem · order theory

AddLECancellable.tsub_lt_iff_tsub_lt

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

Defined in

Mathlib.Algebra.Order.Sub.Unbundled.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommSemigroupPartialOrderExistsAddOfLEAddLeftMonoSubOrderedSub