Theorems · Theorem · order theory
sub_le_sub_right
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, a ≤ b → ∀ (c : α), a - c ≤ b - c- Cited by
- 29 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext
- Assumes
- AddGroupLEAddRightMono
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- AddRightMonostatement and proof · cited by 367
- sub_le_sub_iff_rightproof · cited by 15
Cited by29
Results whose statement or proof uses this declaration.
- Function.hasTemperateGrowth_one_add_norm_sq_rpowproof · cited by 9
- AkraBazziRecurrence.eventually_bi_mul_le_rproof · cited by 4
- Wbtw.trans_left_rightproof · cited by 3
- Manifold.exists_lt_locally_constant_of_riemannianEDist_ltproof · cited by 3
- abs_sub_le_max_subproof · cited by 2
- StieltjesFunction.length_Iocproof · cited by 2
- Real.strictMonoOn_arcoshproof · cited by 2
- Set.Icc.abs_sub_addNSMul_leproof · cited by 2
- CStarModule.inner_mul_inner_swap_leproof · cited by 1
- StieltjesFunction.length_subadditive_Icc_Iooproof · cited by 1
- tendsto_div_of_monotone_of_exists_subseq_tendsto_divproof · cited by 1
- Complex.norm_exp_sub_sum_le_exp_norm_sub_sumproof · cited by 1