Theorems · Theorem · order theory
WithBot.coe_unbot
∀ {α : Type u_1} (x : WithBot α) (hx : x ≠ ⊥), ↑(x.unbot hx) = x- Defined in
- Mathlib.Order.WithBot
- Cited by
- 10 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.
Cites4
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.somestatement and proof · cited by 541
- WithBot.unbotstatement and proof · cited by 23
Cited by10
Results whose statement or proof uses this declaration.
- Finset.le_max'proof · cited by 33
- Finset.coe_sup'proof · cited by 14
- Module.coe_lengthproof · cited by 10
- WithBot.denselyOrdered_set_iff_subsingletonproof · cited by 2
- Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobsonproof · cited by 2
- WithBot.unbot_le_unbot_iffproof · cited by 2
- List.coe_maximum_of_length_posproof · cited by 1
- Order.height_coe_withBotproof · cited by 1
- WithBot.unbot_injproof · cited by 1
- WithBot.unbot_lt_unbot_iffproof · cited by 0