Theorems · Definition · order theory
WithTop.untop
{α : Type u_1} → (x : WithTop α) → x ≠ ⊤ → αDeconstruct a x : WithTop α to the underlying value in α, given a proof that x ≠ ⊤.
- Defined in
- Mathlib.Order.WithBot
- Cited by
- 36 results in Mathlib
- Foundations
- Depth 5 from the axioms · uses no axioms
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.
- Top.topstatement and proof · cited by 9,680
- WithTopstatement and proof · cited by 3,754
- WithTop.someproof · cited by 1,128
Cited by43
Results whose statement or proof uses this declaration.
- Finset.inf'proof · cited by 117
- ENat.liftproof · cited by 19
- WithTop.coe_untopstatement and proof · cited by 17
- HahnSeries.leadingCoeff_of_ne_zerostatement · cited by 11
- WithTop.untop.congr_simpstatement and proof · cited by 9
- List.minimum_of_length_posproof · cited by 5
- WithTop.untop_eq_iffstatement and proof · cited by 4
- WithTop.untop_le_iffstatement · cited by 4
- WithTop.untop_lt_iffstatement · cited by 3
- HahnSeries.leadingCoeff_add_eq_leftproof · cited by 3
- Order.height_coe_withTopproof · cited by 3
- WithTop.iSup_coe_eq_topproof · cited by 3