toDualHomeomorph — Mathlib

English

The Upper Set topology is homeomorphic to the Lower Set topology on the dual order.

Русский

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

LaTeX

$$$ \mathrm{WithUpperSet}(\alpha) \simeq_t \mathrm{WithLowerSet}(\alpha^{\mathrm{op}}).$$$

Lean4

/-- The Upper Set topology is homeomorphic to the Lower Set topology on the dual order
-/
def toDualHomeomorph [Preorder α] : WithUpperSet α ≃ₜ WithLowerSet αᵒᵈ
    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

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