Theorems · Theorem · order theory
le_add_of_nonneg_left
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightMono α] {a b : α}, 0 ≤ b → a ≤ b + a- Cited by
- 37 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
- Assumes
- AddZeroClassLEAddRightMono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- zero_addproof · cited by 2,366
- AddZeroClassstatement and proof · cited by 1,237
- AddRightMonostatement and proof · cited by 367
- add_le_add_leftproof · cited by 37
Cited by37
Results whose statement or proof uses this declaration.
- Finset.sum_le_sum_of_subset_of_nonnegproof · cited by 31
- ProbabilityTheory.integrable_exp_mul_of_le_of_leproof · cited by 7
- segment_eq_imageproof · cited by 7
- max_le_add_of_nonnegproof · cited by 6
- Complex.abs_im_le_normproof · cited by 6
- InnerProductGeometry.sin_angle_add_of_inner_eq_zeroproof · cited by 5
- monotone_iff_map_nonnegproof · cited by 3
- Function.hasTemperateGrowth_norm_sqproof · cited by 3
- cauchySeq_bddproof · cited by 3
- starConvex_zero_iffproof · cited by 2
- Filter.Tendsto.zero_eventuallyLE_add_atTopproof · cited by 2
- Unitization.antilipschitzWith_addEquivproof · cited by 2