Mathlib Map

Theorems · Theorem · order theory

tsub_lt_tsub_left_of_le

∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → c < b → a - b < a - c
Defined in
Mathlib.Algebra.Order.Sub.Unbundled.Basic
Cited by
0 results in Mathlib
Foundations
Depth 12 from the axioms · uses propext, Quot.sound
Assumes
AddCommSemigroupPartialOrderExistsAddOfLEAddLeftMonoSubOrderedSubAddLeftReflectLE
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

PartialOrder · cited by 6410PartialOrderAddLeftMono · cited by 687AddLeftMonoExistsAddOfLE · cited by 330ExistsAddOfLEOrderedSub · cited by 236OrderedSubAddCommSemigroup · cited by 178AddCommSemigroupAddLeftReflectLE · cited by 119AddLeftReflectLEContravariant.AddLECancellable · cited by 45Contravariant.AddLECancel…AddLECancellable.tsub_lt_tsub_left_of_le · cited by 2AddLECancellable.tsub_lt_…tsub_lt_tsub_left_of_leCITED BYCITES

Cites8

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.