Theorems · Theorem · order theory
max_lt_iff
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max b c < a ↔ b < a ∧ c < a- Defined in
- Mathlib.Order.MinMax
- Cited by
- 22 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
- sup_lt_iffproof · cited by 9
Cited by22
Results whose statement or proof uses this declaration.
- abs_ltproof · cited by 43
- Polynomial.div_modByMonic_uniqueproof · cited by 12
- Polynomial.degree_sub_lt_leftproof · cited by 9
- mabs_ltproof · cited by 4
- comap_coe_nhdsLT_of_Ioo_subsetproof · cited by 3
- cauchySeq_of_edist_le_of_summableproof · cited by 2
- not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioiproof · cited by 2
- isBigO_norm_Icc_restrict_atTopproof · cited by 2
- Set.notMem_uIcc_of_gtproof · cited by 2
- Multipliable.eventually_bounded_finsetProdproof · cited by 2
- intervalIntegral.continuous_parametric_primitive_of_continuousproof · cited by 1