English
There is a natural equivalence between the non-bottom elements of WithBot α and α, given by unbot on the forward side and some on the backward side.
Русский
Существует естественное биективное соответствие между ненижними элементами WithBot α и α, задаваемоеUnbot в прямом направлении и Some в обратном.
LaTeX
$$$\operatorname{Equiv.withBotSubtypeNe} : \{ y : WithBot α \mid y \neq ⊥ \} \simeq α$$$
Lean4
/-- The equivalence between the non-bottom elements of `WithBot α` and `α`. -/
@[simps]
def _root_.Equiv.withBotSubtypeNe : { y : WithBot α // y ≠ ⊥ } ≃ α
where
toFun := fun ⟨x, h⟩ => WithBot.unbot x h
invFun x := ⟨x, WithBot.coe_ne_bot⟩
left_inv _ := by simp
right_inv _ := by simp
