English
There is an order isomorphism between WithTop of a subtype excluding top and α.
Русский
Существует изоморфизм упорядочений между WithTop {a ∈ α | a ≠ ⊤} и α.
LaTeX
$$WithTop \\{a : α | a ≠ ⊤\\} ≃o α$$
Lean4
/-- Any `OrderTop` is equivalent to `WithTop` of the subtype excluding `⊤`.
See also `Equiv.optionSubtypeNe`. -/
def subtypeOrderIso [PartialOrder α] [OrderTop α] [DecidablePred (· = (⊤ : α))] : WithTop { a : α // a ≠ ⊤ } ≃o α
where
toFun a := (a.map (↑)).untopD ⊤
invFun a := if h : a = ⊤ then ⊤ else .some ⟨a, h⟩
left_inv
| .some ⟨a, h⟩ => by simp [h]
| ⊤ => by simp
right_inv a := by dsimp only; split_ifs <;> simp [*]
map_rel_iff'
{a b} :=
match a, b with
| .some a, .some b => by simp
| ⊤, .some ⟨b, h⟩ => by simp [h]
| a, ⊤ => by simp
