English
There is a natural bijection between the non-top elements of WithTop(α) and α, given by mapping ⟨x,h⟩ ↦ WithTop.untop x h with inverse x ↦ ⟨x, WithTop.coe_ne_top⟩.
Русский
Существует естественная биекция между не-верхними элементами WithTop(α) и α, заданная отображением ⟨x,h⟩ ↦ WithTop.untop x h и обратной связью x ↦ ⟨x, WithTop.coe_ne_top⟩.
LaTeX
$$$\{ y : \mathrm{WithTop}(\alpha) \mid y \neq \top \} \cong \alpha$$$
Lean4
/-- The equivalence between the non-top elements of `WithTop α` and `α`. -/
@[simps]
def _root_.Equiv.withTopSubtypeNe : { y : WithTop α // y ≠ ⊤ } ≃ α
where
toFun := fun ⟨x, h⟩ => WithTop.untop x h
invFun x := ⟨x, WithTop.coe_ne_top⟩
left_inv _ := by simp
right_inv _ := by simp
