feat(topology/homeomorph): Add homeomorph_of_continuous_equiv

[callesonne]

Add definitions homeomorph_of_continuous_closed and homeomorph_of_continuous_equiv

---

[jcommelin]

Thanks. Could you please add some API around these defs? This might be as easy as adding @[simps] before def.

[callesonne]

Thanks. Could you please add some API around these defs? This might be as easy as adding @[simps] before def.

Like in the new commit? I dont get exactly what you mean by "API" in this context.

[urkud]

This way (homeomorph_of_continuous_closed e h₁ h₂).to_equiv = e is a rfl:

Suggested change

	.. e }
	to_equiv := e }

[urkud]

@jcommelin @[simps] doesn't work for homeomorph because it is a new structure with h.to_fun = h.to_equiv.to_fun.
@callesonne With @[simp] attributes, simp will always unfold these definitions. If you only want to unfold them if they're applied, then you can add lemmas like @[simp] homeomorph_of_continuous_coe : ⇑(homeomorph_of_continuous e h) = e := rfl, @[simp] homeomorph_of_continuous_symm_coe : ⇑(homeomorph_of_continuous e h).symm = e.symm := rfl and @[simp] homeomorph_of_continuous_to_equiv : (homeomorph_of_continuous e h).to_equiv = e := rfl.

[jcommelin]

Aha, so @[simps] doesn't work. @callesonne please add lemmas like the ones that Yury suggested above.

[callesonne]

Okay, so what about homeomorph_of_continuous_closed? Comparing with homeomorph_of_continuous_open (which was there before) it has no API that I can see, should I add an API for this one as well?

[urkud]

In the meantime, an equivalent statement was merged into master. So, I'm going to close this PR.