Theorems · Theorem · order theory
le_imp_le_of_le_of_le
∀ {α : Type u_2} [inst : Preorder α] {a b c d : α}, c ≤ a → b ≤ d → a ≤ b → c ≤ dmonotonicity of ≤ with respect to →
- Defined in
- Mathlib.Order.Basic
- Cited by
- 576 results in Mathlib
- Foundations
- Depth 5 from the axioms, rests on 4 definitions · uses no axioms
- Assumes
- Preorder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Preorderstatement and proof · cited by 7,952
- LE.le.transproof · cited by 3,151
Cited by576
Results whose statement or proof uses this declaration.
- add_le_addproof · cited by 666
- mul_le_mul'proof · cited by 274
- add_tsub_cancel_of_leproof · cited by 79
- tsub_le_tsub_leftproof · cited by 15
- Topology.IsInducing.of_compproof · cited by 11
- Set.image2_inter_union_subset_unionproof · cited by 10
- Set.image2_union_inter_subset_unionproof · cited by 9
- MeasureTheory.IsSetSemiring.exists_finpartition_sdiffproof · cited by 8
- add_le_of_le_tsub_right_of_leproof · cited by 8
- ONote.NFBelow.repr_ltproof · cited by 7
- MeasureTheory.Integrable.integral_prod_leftproof · cited by 7
- MonovaryOn.sum_smul_comp_perm_le_sum_smulproof · cited by 7
Showing the 200 most cited of 576.