Theorems · Theorem · order theory
sub_le_sub_left
∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddLeftMono α] [AddRightMono α] {a b : α},
a ≤ b → ∀ (c : α), c - b ≤ c - a- Cited by
- 43 results in Mathlib
- Foundations
- Depth 16 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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
- AddLeftMonostatement and proof · cited by 687
- AddRightMonostatement and proof · cited by 367
- sub_le_sub_iff_leftproof · cited by 8
Cited by43
Results whose statement or proof uses this declaration.
- ProbabilityTheory.sub_half_inf_sub_mem_Iooproof · cited by 4
- AkraBazziRecurrence.eventually_bi_mul_le_rproof · cited by 4
- HasFPowerSeriesWithinOnBall.uniform_geometric_approx'proof · cited by 3
- UpperHalfPlane.im_pos_of_dist_center_leproof · cited by 3
- Int.abs_sub_lt_one_of_floor_eq_floorproof · cited by 3
- abs_sub_le_max_subproof · cited by 2
- Asymptotics.IsBigOWith.right_le_sub_of_lt_oneproof · cited by 2
- StieltjesFunction.length_Iocproof · cited by 2
- Unitary.norm_sub_one_sq_eqproof · cited by 2
- CFC.monotoneOn_one_sub_one_add_invproof · cited by 2
- MeasureTheory.exists_lt_lowerSemicontinuous_integral_ltproof · cited by 2
- Complex.norm_sub_mem_Icc_angleproof · cited by 2