Theorems · Definition · order theory
WithTop.untopD
{α : Type u_1} → α → WithTop α → αSpecialization of Option.getD to values in WithTop α that respects API boundaries.
- Defined in
- Mathlib.Order.WithBot
- Cited by
- 33 results in Mathlib
- Foundations
- Depth 6 from the axioms · uses no axioms
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.
- WithTopstatement and proof · cited by 3,754
- WithTop.recTopCoeproof · cited by 107
Cited by41
Results whose statement or proof uses this declaration.
- ENNReal.toNNRealproof · cited by 165
- ENat.toNatproof · cited by 143
- multiplicityproof · cited by 117
- WithTop.untop₀proof · cited by 73
- WithTop.untopAproof · cited by 37
- SimpleGraph.minDegreeproof · cited by 25
- meromorphicOrderAt_ne_top_iffproof · cited by 11
- multiplicity_eq_of_emultiplicity_eq_someproof · cited by 11
- multiplicity_eq_of_emultiplicity_eqproof · cited by 8
- Polynomial.rootMultiplicity_eq_multiplicityproof · cited by 8
- SimpleGraph.minDegree_of_subsingletonproof · cited by 6
- multiplicity_eq_one_of_not_finiteMultiplicityproof · cited by 4