Theorems · Theorem · order theory
add_le_add_iff_left
∀ {α : Type u_1} [inst : Add α] [inst_1 : LE α] [AddLeftMono α] [AddLeftReflectLE α] (a : α) {b c : α},
a + b ≤ a + c ↔ b ≤ c- Cited by
- 45 results in Mathlib
- Foundations
- Depth 5 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.
- AddLeftMonostatement and proof · cited by 687
- AddLeftReflectLEstatement and proof · cited by 119
- CovariantClass.elimproof · cited by 22
- rel_iff_cov'proof · cited by 5
- AddLeftReflectLE.le_of_add_le_add_leftproof · cited by 2
Cited by45
Results whose statement or proof uses this declaration.
- neg_le_neg_iffproof · cited by 57
- le_add_iff_nonneg_rightproof · cited by 15
- Left.neg_nonpos_iffproof · cited by 14
- Left.nonneg_neg_iffproof · cited by 14
- add_le_iff_nonpos_rightproof · cited by 9
- sub_le_sub_iff_leftproof · cited by 8
- neg_add_le_iff_le_addproof · cited by 6
- Ordinal.sub_leproof · cited by 5
- Ordinal.mul_add_divproof · cited by 4
- RootPairing.isCompl_rootSpan_ker_rootFormproof · cited by 4
- neg_le_iff_add_nonneg'proof · cited by 3
- Pell.exists_of_not_isSquareproof · cited by 3