Theorems · Definition · order theory
WithBot.unbot
{α : Type u_1} → (x : WithBot α) → x ≠ ⊥ → αDeconstruct a x : WithBot α to the underlying value in α, given a proof that x ≠ ⊥.
- Defined in
- Mathlib.Order.WithBot
- Cited by
- 23 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.
- Bot.botstatement and proof · cited by 4,720
- WithBotstatement and proof · cited by 1,498
- WithBot.someproof · cited by 541
Cited by27
Results whose statement or proof uses this declaration.
- Finset.sup'proof · cited by 174
- Module.lengthproof · cited by 56
- WithBot.coe_unbotstatement and proof · cited by 10
- List.maximum_of_length_posproof · cited by 7
- Module.length_eq_of_surjectiveproof · cited by 4
- WithBot.lt_unbot_iffstatement · cited by 2
- WithBot.denselyOrdered_set_iff_subsingletonproof · cited by 2
- Equiv.withBotSubtypeNeproof · cited by 2
- WithBot.le_unbot_iffstatement · cited by 2
- WithBot.unbot_le_unbot_iffstatement · cited by 2
- WithBot.tendsto_unbotstatement and proof · cited by 1
- WithBot.unbotA_eq_unbotstatement · cited by 1