WithLowerSetHomeomorph — Mathlib

English

There is a natural homeomorphism between the lower-set extension of α and α itself when α is equipped with the lower-set topology.

Русский

Существует естественный гомеоморфизм между расширением нижних множеств α и самим α, если задана нижняя топология.

LaTeX

$$$$ \\mathrm{WithLowerSet}(\\alpha) \\simeq_{\\mathrm{Top}} \\alpha. $$$$

Lean4

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

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