Theorems · Theorem · order theory
sub_nonneg
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, 0 ≤ a - b ↔ b ≤ a- Cited by
- 167 results in Mathlib
- Foundations
- Depth 14 from the axioms, rests on 64 definitions · uses propext
- Assumes
- AddGroupLEAddRightMono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- zero_addproof · cited by 2,366
- sub_eq_add_negproof · cited by 1,023
- AddRightMonostatement and proof · cited by 367
- neg_add_cancel_rightproof · cited by 75
- add_le_add_iff_rightproof · cited by 47
Cited by167
Results whose statement or proof uses this declaration.
- sub_nonneg_of_leproof · cited by 37
- Int.cast_leproof · cited by 28
- Int.fract_nonnegproof · cited by 17
- MeasureTheory.integral_mono_aeproof · cited by 15
- Real.hasDerivAt_rpow_constproof · cited by 11
- Unitization.inr_le_iffproof · cited by 8
- segment_eq_imageproof · cited by 7
- Real.sin_pi_over_two_pow_succproof · cited by 6
- EuclideanGeometry.angle_eq_pi_iff_sbtwproof · cited by 6
- Function.locallyFinsuppWithin.logCounting_leproof · cited by 5
- HurwitzKernelBounds.summable_f_natproof · cited by 5
- Real.sin_eq_zero_iffproof · cited by 5