OnePoint Homeomorph

Stream: Is there code for X?

[Bjørn Kjos-Hanssen]

Is there already code making it quick to prove this simple statement?

import Mathlib

example (X Y : Type*) [TopologicalSpace X] [TopologicalSpace Y]
  (h : Homeomorph X Y):
    Homeomorph (OnePoint X) (OnePoint Y) := by sorry

(More generally, to prove that various operations on topologies are closed under homeomorphism.)

[Jireh Loreaux]

It should be pretty easy with docs#OnePoint.equivOfIsEmbeddingOfRangeEq

[Bjørn Kjos-Hanssen]

Thanks, got it to work, except I had to assume [T2Space Y] [LocallyCompactSpace Y].

[Yury G. Kudryashov]

#18644

[Bjørn Kjos-Hanssen]

... and now I don't have to assume that. Thanks!