withUpperHomeomorph — Mathlib

English

If α is equipped with the upper topology, then it is homeomorphic to WithUpper α.

Русский

Если на α задана верхняя топология, то α гомеоморфно WithUpper α.

LaTeX

$$$\\text{WithUpper}(\\alpha) \\simeq_{\\text{Homeomorphism}} \\alpha$$$

Lean4

/-- If `α` is equipped with the upper topology, then it is homeomorphic to `WithUpper α`.
-/
def withUpperHomeomorph : WithUpper α ≃ₜ α :=
  WithUpper.ofUpper.toHomeomorphOfIsInducing ⟨topology_eq α ▸ induced_id.symm⟩

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