IciBot — Mathlib

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 }

Похожие утверждения