English
There is an order isomorphism between the half-open interval Ici(⊥) and the ambient preorder α, given α has a bottom element.
Русский
Существует изоморфизм порядка между Ici(⊥) и исходной порядковой структурой α, если в α есть нижняя граница.
LaTeX
$$$$ IciBot : Ici(\bot) \cong_o \alpha $$$$
Lean4
/-- Order isomorphism between `Ici (⊥ : α)` and `α` when `α` has a bottom element -/
def IciBot {α : Type*} [Preorder α] [OrderBot α] : Ici (⊥ : α) ≃o α :=
{ @Equiv.subtypeUnivEquiv α (Ici (⊥ : α)) fun _ => bot_le with map_rel_iff' := @fun x y => by rfl }