IicTop — Mathlib

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 }

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