Theorems · Theorem · order theory
tsub_le_iff_right
∀ {α : Type u_1} [inst : LE α] [inst_1 : Add α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}, a - b ≤ c ↔ a ≤ c + b- Defined in
- Mathlib.Algebra.Order.Sub.Defs
- Cited by
- 49 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
- Assumes
- LEAddSubOrderedSub
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- OrderedSubstatement and proof · cited by 236
- OrderedSub.tsub_le_iff_rightproof · cited by 1
Cited by49
Results whose statement or proof uses this declaration.
- tsub_le_iff_leftproof · cited by 38
- lt_tsub_iff_rightproof · cited by 16
- AddLECancellable.tsub_eq_of_eq_addproof · cited by 11
- le_tsub_addproof · cited by 10
- ENNReal.iInf_addproof · cited by 7
- add_tsub_add_eq_tsub_rightproof · cited by 5
- ENat.iInf_addproof · cited by 5
- tsub_le_iff_tsub_leproof · cited by 5
- continuous_of_le_add_edistproof · cited by 4
- infEDist_thickeningproof · cited by 3
- NNReal.nndist_eqproof · cited by 3
- AddHom.le_map_tsubproof · cited by 3