Theorems · Theorem · order theory
min_eq_left
∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → min a b = a- Defined in
- Mathlib.Order.Defs.LinearOrder
- Cited by
- 67 results in Mathlib
- Foundations
- Depth 11 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
- le_rflproof · cited by 1,558
- eq_minproof · cited by 3
Cited by67
Results whose statement or proof uses this declaration.
- lt_minproof · cited by 69
- min_eq_rightproof · cited by 54
- intervalIntegral.integral_eq_sub_of_hasDeriv_rightproof · cited by 8
- MeasureTheory.stoppedProcess_stoppedProcessproof · cited by 6
- intervalIntegral.continuousWithinAt_primitiveproof · cited by 6
- integral_cpowproof · cited by 5
- min_eq_left_of_ltproof · cited by 4
- ProbabilityTheory.IsGaussianProcess.isPreBrownianReal_of_covarianceproof · cited by 4
- AddCircle.volume_closedBallproof · cited by 4
- SimpleGraph.IsTuranMaximal.nonempty_iso_turanGraphproof · cited by 3
- padicValRat.min_le_padicValRat_addproof · cited by 3
- max_sub_min_eq_abs'proof · cited by 3