homeomorph — Mathlib

English

There exists a homeomorphism between X and Shrink(X).

Русский

Существует гомеоморфизм между X и Shrink(X).

LaTeX

$$$X \\cong_{\\text{Top}} \\mathrm{Shrink}(X).$$$

Lean4

/-- `equivShrink` as a homeomorphism. -/
@[simps toEquiv]
noncomputable def homeomorph (X : Type u) [TopologicalSpace X] [Small.{v} X] : X ≃ₜ Shrink.{v} X
    where
  __ := equivShrink X
  continuous_toFun := continuous_coinduced_rng
  continuous_invFun := by
    convert continuous_induced_dom
    simp only [Equiv.invFun_as_coe, Equiv.induced_symm]
    rfl

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