Theorems · Theorem · general topology

Homeomorph.continuous_invFun

∀ {X : Type u_5} {Y : Type u_6} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (self : X ≃ₜ Y),
  Continuous self.invFun

The inverse map of a homeomorphism is a continuous function.

Defined in

Mathlib.Topology.Homeomorph.Defs

Cited by

3 results in Mathlib

Foundations

Depth 3 from the axioms · uses no axioms

Assumes

TopologicalSpaceTopologicalSpace