Theorems · Theorem · order theory
le_add_iff_nonneg_left
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddRightMono α] [AddRightReflectLE α] (a : α) {b : α},
a ≤ b + a ↔ 0 ≤ b- Cited by
- 12 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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.
- zero_addproof · cited by 2,366
- AddZeroClassstatement and proof · cited by 1,237
- AddRightMonostatement and proof · cited by 367
- AddRightReflectLEstatement and proof · cited by 53
- add_le_add_iff_rightproof · cited by 47
Cited by12
Results whose statement or proof uses this declaration.
- wbtw_smul_vadd_smul_vadd_of_nonpos_of_nonnegproof · cited by 2
- Seminorm.finset_sup_le_sumproof · cited by 2
- ProbabilityTheory.integrable_exp_mul_abs_addproof · cited by 2
- geom_sum_alternating_of_le_neg_oneproof · cited by 1
- IsNonarchimedean.add_leproof · cited by 1
- half_le_self_iffproof · cited by 1
- Liouville.exists_pos_real_of_irrational_rootproof · cited by 1
- Real.norm_deriv_mulExpNegMulSq_le_oneproof · cited by 1
- Finset.sum_Icc_of_even_eq_rangeproof · cited by 0
- Finset.sum_Icc_succ_eq_add_endpointsproof · cited by 0
- card_Ico_zero_addproof · cited by 0
- Finset.sum_Ico_int_subproof · cited by 0