Theorems · Theorem · order theory
sub_le_sub
∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : Preorder α] [AddLeftMono α] {a b c d : α},
a ≤ b → c ≤ d → a - d ≤ b - c- Cited by
- 24 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites7
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddCommGroupstatement and proof · cited by 12,871
- Preorderstatement and proof · cited by 7,952
- add_commproof · cited by 1,535
- sub_eq_add_negproof · cited by 1,023
- AddLeftMonostatement and proof · cited by 687
- add_le_addproof · cited by 666
- add_neg_le_neg_add_iffproof · cited by 3
Cited by24
Results whose statement or proof uses this declaration.
- lt_or_lt_of_sub_lt_subproof · cited by 4
- MonotoneOn.eVariationOn_eqproof · cited by 4
- Set.abs_sub_le_of_uIcc_subset_uIccproof · cited by 3
- Chebyshev.psi_ge'proof · cited by 2
- sub_inv_antitoneOn_Iioproof · cited by 2
- sub_inv_antitoneOn_Ioiproof · cited by 2
- AntilipschitzWith.add_lipschitzWithproof · cited by 2
- abs_sub_le_of_le_of_leproof · cited by 1
- tendsto_div_of_monotone_of_exists_subseq_tendsto_divproof · cited by 1
- GaussianFourier.verticalIntegral_norm_leproof · cited by 1
- Finset.card_mul_finset_lt_twoproof · cited by 1
- AntilipschitzWith.mul_lipschitzWithproof · cited by 1