Theorems · Theorem · order theory
le_max_of_le_right
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a ≤ c → a ≤ max b c- Defined in
- Mathlib.Order.MinMax
- Cited by
- 30 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_rightproof · cited by 17
Cited by30
Results whose statement or proof uses this declaration.
- intervalIntegral.continuousWithinAt_primitiveproof · cited by 6
- NumberField.hermiteTheorem.rank_le_rankOfDiscrBddproof · cited by 4
- PhragmenLindelof.quadrant_Iproof · cited by 4
- Filter.Tendsto.atTop_mul_const'proof · cited by 3
- Metric.hausdorffEDist_iUnion_leproof · cited by 2
- abs_sub_le_max_subproof · cited by 2
- Filter.Tendsto.const_mul_atTop'proof · cited by 2
- FreeAlgebra.cardinalMk_le_max_liftproof · cited by 2
- IsAlgClosed.cardinal_eq_cardinal_transcendence_basis_of_aleph0_ltproof · cited by 2
- dist_integral_mulExpNegMulSq_comp_leproof · cited by 1
- bdd_le_mul_tendsto_zeroproof · cited by 1
- tendsto_tsum_div_pow_atTop_integralproof · cited by 1