Theorems · Theorem · order theory
add_le_add
∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α] {a b c d : α},
a ≤ b → c ≤ d → a + c ≤ b + d- Cited by
- 666 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 15 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
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
- le_reflproof · cited by 2,061
- AddLeftMonostatement and proof · cited by 687
- le_imp_le_of_le_of_leproof · cited by 576
- AddRightMonostatement and proof · cited by 367
- add_le_add_leftproof · cited by 37
- add_le_add_rightproof · cited by 37
Cited by666
Results whose statement or proof uses this declaration.
- add_tsub_cancel_of_leproof · cited by 79
- sub_le_subproof · cited by 24
- MeasureTheory.lintegral_add_leftproof · cited by 21
- Metric.isBounded_closedBallproof · cited by 19
- abs_add_leproof · cited by 17
- tsub_le_tsub_leftproof · cited by 15
- Polynomial.natDegree_mul_leproof · cited by 15
- MeasureTheory.ae_of_ae_restrict_of_ae_restrict_complproof · cited by 14
- MeasureTheory.lintegral_add_measureproof · cited by 13
- Cardinal.add_eq_maxproof · cited by 13
- MeasureTheory.measure_sdiff_nullproof · cited by 13
- norm_add_le_of_leproof · cited by 13
Showing the 200 most cited of 666.