withScottHomeomorph — Mathlib

English

If α is IsScott univ, then WithScott α is homeomorphic to α.

Русский

Если α является IsScott на univ, то WithScott α гомеоморфно α.

LaTeX

$$$WithScott(\alpha) \simeq_{\mathrm{Homeo}} \alpha.$$$

Lean4

/-- If `α` is equipped with the Scott topology, then it is homeomorphic to `WithScott α`.
-/
def withScottHomeomorph [IsScott α univ] : WithScott α ≃ₜ α :=
  WithScott.ofScott.toHomeomorphOfIsInducing ⟨IsScott.topology_eq α univ ▸ induced_id.symm⟩

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