Theorems · Theorem · order theory
le_max_of_le_left
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ b → a ≤ max b c- Defined in
- Mathlib.Order.MinMax
- Cited by
- 31 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- LinearOrder
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.
- LinearOrderstatement and proof · cited by 8,572
- le_sup_of_le_leftproof · cited by 26
Cited by31
Results whose statement or proof uses this declaration.
- NumberField.hermiteTheorem.rank_le_rankOfDiscrBddproof · cited by 4
- BoundedContinuousFunction.norm_add_eq_maxproof · cited by 3
- MultilinearMap.norm_image_sub_le_of_boundproof · cited by 3
- Height.mulHeight_eval_leproof · cited by 3
- Metric.hausdorffEDist_iUnion_leproof · cited by 2
- abs_sub_le_max_subproof · cited by 2
- ODE.FunSpace.dist_iterate_next_iterate_next_leproof · cited by 2
- ODE.FunSpace.exists_contractingWith_iterate_nextproof · cited by 2
- Unitization.antilipschitzWith_addEquivproof · cited by 2
- NNReal.bddAbove_coeproof · cited by 2
- FreeAlgebra.cardinalMk_le_max_liftproof · cited by 2
- Unitization.lipschitzWith_addEquivproof · cited by 2