Theorems · Theorem · order theory
add_le_iff_nonpos_right
∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b : α},
a + b ≤ a ↔ b ≤ 0- Cited by
- 9 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 by9
Results whose statement or proof uses this declaration.
- Finset.sum_eq_sum_Ico_succ_botproof · cited by 8
- sub_le_self_iffproof · cited by 7
- AddSubgroup.exists_nsmul_mem_of_index_ne_zeroproof · cited by 2
- alternatingGroup.mem_kleinFour_of_order_two_powproof · cited by 1
- tendsto_integral_mul_one_add_inv_smul_sq_powproof · cited by 1
- Polynomial.not_finiteproof · cited by 1
- MvPolynomial.irreducible_of_forall_totalDegree_leproof · cited by 1
- Finset.sum_Icc_of_even_eq_rangeproof · cited by 0
- Finset.sum_Icc_succ_eq_add_endpointsproof · cited by 0