Transfer topological structure across Equivs

We show how to transport a topological space structure across an Equiv and prove that this make the equivalence a homeomorphism between the original space and the transported topology.

@[reducible, inline]

abbrev Equiv.topologicalSpace {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (e : α ≃ β) : TopologicalSpace α

Transfer a TopologicalSpace across an Equiv

Equations

• e.topologicalSpace = TopologicalSpace.induced (⇑e) inst✝

def Equiv.homeomorph {α : Type u_2} {β : Type u_3} [TopologicalSpace β] (e : α ≃ β) : α ≃ₜ β

An equivalence e : α ≃ β gives a homeomorphism α ≃ₜ β where the topological space structure on α is the one obtained by transporting the topological space structure on β back along e.

Equations

• e.homeomorph = { toEquiv := e, continuous_toFun := ⋯, continuous_invFun := ⋯ }