Theorems · Theorem · order theory
tsub_le_iff_left
∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α},
a - b ≤ c ↔ a ≤ b + c- Defined in
- Mathlib.Algebra.Order.Sub.Defs
- Cited by
- 38 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- add_commproof · cited by 1,535
- OrderedSubstatement and proof · cited by 236
- AddCommSemigroupstatement and proof · cited by 178
- tsub_le_iff_rightproof · cited by 49
Cited by38
Results whose statement or proof uses this declaration.
- tsub_eq_zero_iff_leproof · cited by 32
- tsub_le_selfproof · cited by 22
- MeasureTheory.lintegral_add_leftproof · cited by 21
- tsub_le_tsub_rightproof · cited by 16
- tsub_le_tsub_leftproof · cited by 15
- le_add_tsubproof · cited by 14
- tsub_tsubproof · cited by 9
- MeasureTheory.le_measure_sdiffproof · cited by 8
- lt_tsub_iff_leftproof · cited by 6
- tsub_le_iff_tsub_leproof · cited by 5
- SzemerediRegularity.a_add_one_le_four_pow_parts_cardproof · cited by 4
- AddLECancellable.tsub_le_tsub_iff_leftproof · cited by 4