Theorems · Theorem · order theory
le_add_iff_nonneg_right
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b : α},
a ≤ a + b ↔ 0 ≤ b- Cited by
- 15 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.
- add_zeroproof · cited by 2,707
- AddZeroClassstatement and proof · cited by 1,237
- AddLeftMonostatement and proof · cited by 687
- AddLeftReflectLEstatement and proof · cited by 119
- add_le_add_iff_leftproof · cited by 45
Cited by15
Results whose statement or proof uses this declaration.
- Function.HasTemperateGrowth.addproof · cited by 4
- EuclideanGeometry.Sphere.IsTangent.radius_le_dist_centerproof · cited by 3
- le_sub_self_iffproof · cited by 2
- IsLUB.mul_leftproof · cited by 2
- ProbabilityTheory.integrable_exp_mul_abs_addproof · cited by 2
- IsNonarchimedean.add_leproof · cited by 1
- norm_eq_iInf_iff_real_inner_le_zeroproof · cited by 1
- mem_adjoin_of_smul_prime_smul_of_minpoly_isEisensteinAtproof · cited by 1
- Finset.sum_range_diag_flipproof · cited by 1
- Finset.card_Ico_add_rightproof · cited by 1
- IsStrictlyPositive.add_nonnegproof · cited by 1
- CauSeq.trichotomyproof · cited by 1