Theorems · Theorem · general topology

Homeomorph.symm_comp_toContinuousMap

∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β),
  (↑f.symm).comp ↑f = ContinuousMap.id α

Left inverse to a continuous map from a homeomorphism, mirroring Equiv.symm_comp_self.

Defined in

Mathlib.Topology.ContinuousMap.Basic

Cited by

1 results in Mathlib

Foundations

Depth 18 from the axioms · uses Quot.sound

Assumes

TopologicalSpaceTopologicalSpace