Theorems · Theorem · order theory
lt_max_of_lt_left
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < b → a < max b c- Defined in
- Mathlib.Order.MinMax
- Cited by
- 16 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.
Cites3
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
- LT.lt.trans_leproof · cited by 678
- le_max_leftproof · cited by 215
Cited by16
Results whose statement or proof uses this declaration.
- Polynomial.norm_coeff_le_choose_mul_mahlerMeasureproof · cited by 3
- Ordinal.IsPrincipal.sSupproof · cited by 2
- ProbabilityTheory.rpow_abs_le_mul_max_exp_of_posproof · cited by 2
- dist_integral_mulExpNegMulSq_comp_leproof · cited by 1
- AkraBazziRecurrence.eventually_atTop_sumTransform_leproof · cited by 1
- NumberField.hermiteTheorem.finite_of_discr_bdd_of_isComplexproof · cited by 1
- NumberField.hermiteTheorem.finite_of_discr_bdd_of_isRealproof · cited by 1
- Int.Matrix.exists_ne_zero_int_vec_norm_leproof · cited by 1
- Complex.HadamardThreeLines.F_BddAboveproof · cited by 1
- MeasureTheory.AECover.integrable_of_lintegral_enorm_tendstoproof · cited by 1
- Frullani.tendsto_integral_inv_smul_nhdsWithinproof · cited by 1