withLowerHomeomorph — Mathlib

English

If α is equipped with the lower topology, then α is homeomorphic to WithLower α.

Русский

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

LaTeX

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

Lean4

/-- If `α` is equipped with the lower topology, then it is homeomorphic to `WithLower α`.
-/
def withLowerHomeomorph : WithLower α ≃ₜ α :=
  WithLower.ofLower.toHomeomorphOfIsInducing ⟨topology_eq α ▸ induced_id.symm⟩

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