toHomeomorphOfIsInducing — Mathlib

English

An inducing equivalence between topological spaces is a homeomorphism.

Русский

Индуцирующее эквиваленто между топологическими пространствами является гомеоморфизмом.

LaTeX

$$$ \\text{toHomeomorphOfIsInducing}(f, hf) : X \\toHomeomorph Y \\;\\text{is a homeomorphism}$$$

Lean4

/-- An inducing equiv between topological spaces is a homeomorphism. -/
@[simps toEquiv]
def toHomeomorphOfIsInducing (f : X ≃ Y) (hf : IsInducing f) : X ≃ₜ Y :=
  { f with
    continuous_toFun := hf.continuous
    continuous_invFun := hf.continuous_iff.2 <| by simpa using continuous_id }

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