English
There is an order isomorphism between the closed lower interval Iic(⊤) and the ambient preorder α, provided α has a top element.
Русский
Существует изоморфизм порядка между замкнутым нижним интервалом Iic(⊤) и исходной порядковой структурой α, если у α есть верх.
LaTeX
$$$$ IicTop : Iic(\top) \cong_o \alpha $$$$
Lean4
/-- Order isomorphism between `Iic (⊤ : α)` and `α` when `α` has a top element -/
def IicTop {α : Type*} [Preorder α] [OrderTop α] : Iic (⊤ : α) ≃o α :=
{ @Equiv.subtypeUnivEquiv α (Iic (⊤ : α)) fun _ => le_top with map_rel_iff' := @fun x y => by rfl }