toDualHomeomorph — Mathlib

English

The lower topology on α is homeomorphic to the upper topology on the dual order αᵒᵈ.

Русский

Нижняя топология на α гомеоморфна верхней топологии на двойственном порядке αᵒᵈ.

LaTeX

$$$\\mathrm{WithLower} \\alpha \\simeq_{t} \\mathrm{WithUpper}(\\alpha^{\\mathrm{op}})$$$

Lean4

/-- The lower topology is homeomorphic to the upper topology on the dual order
-/
def toDualHomeomorph [Preorder α] : WithLower α ≃ₜ WithUpper αᵒᵈ
    where
  toFun := OrderDual.toDual
  invFun := OrderDual.ofDual
  left_inv := OrderDual.toDual_ofDual
  right_inv := OrderDual.ofDual_toDual
  continuous_toFun := continuous_coinduced_rng
  continuous_invFun := continuous_coinduced_rng

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