Theorems · Theorem · order theory

tsub_lt_tsub_iff_left_of_le

∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedAdd α] [inst_3 : Sub α]
  [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → (a - b < a - c ↔ c < b)

See lt_tsub_iff_left_of_le_of_le for a weaker statement in a partial order.

Defined in

Mathlib.Algebra.Order.Sub.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

AddCommMonoidLinearOrderCanonicallyOrderedAddSubOrderedSubAddLeftReflectLE