Theorems · Theorem · order theory
max_self
∀ {α : Type u_1} [inst : LinearOrder α] (a : α), max a a = a- Defined in
- Mathlib.Order.Defs.LinearOrder
- Cited by
- 43 results in Mathlib
- Foundations
- Depth 12 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
- max_def'proof · cited by 7
Cited by43
Results whose statement or proof uses this declaration.
- IsBoundedBilinearMap.hasStrictFDerivAtproof · cited by 7
- Metric.hausdorffEDist_singletonproof · cited by 5
- Real.posLog_mulproof · cited by 3
- Ordinal.card_opow_le_of_omega0_le_leftproof · cited by 3
- ProbabilityTheory.BrownianReal.posSemidef_covMatrixproof · cited by 2
- Real.posLog_oneproof · cited by 2
- Valuation.map_sub_of_left_eq_zeroproof · cited by 2
- Real.posLog_sumproof · cited by 2
- RatFunc.natDegree_minpolyXproof · cited by 2
- Height.mulHeight₁_oneproof · cited by 2
- Cardinal.mk_perm_eq_self_powerproof · cited by 2
- Valuation.isEquiv_iff_val_eq_oneproof · cited by 2