Theorems · Theorem · order theory
lt_min_iff
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, a < min b c ↔ a < b ∧ a < c- Defined in
- Mathlib.Order.MinMax
- Cited by
- 14 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
- lt_inf_iffproof · cited by 7
Cited by14
Results whose statement or proof uses this declaration.
- Set.notMem_uIcc_of_ltproof · cited by 6
- ArchimedeanClass.min_le_mk_addproof · cited by 5
- MulArchimedeanClass.min_le_mk_mulproof · cited by 4
- FormalMultilinearSeries.min_radius_le_radius_addproof · cited by 2
- closure_ordConnected_inter_ratproof · cited by 1
- intervalIntegral.continuous_parametric_primitive_of_continuousproof · cited by 1
- PiNat.min_firstDiff_leproof · cited by 1
- FormalMultilinearSeries.radius_prod_eq_minproof · cited by 1
- ProbabilityTheory.measure_le_mul_measure_gt_le_of_map_rotation_eq_selfproof · cited by 1
- ENNReal.tendsto_atTop_zero_iff_lt_of_antitoneproof · cited by 1
- SimpleGraph.IsTuranMaximal.card_partsproof · cited by 1
- ContinuousMap.dense_setOfPred_contDiffproof · cited by 1