[Merged by Bors] - feat(topology/connected): sufficient conditions for the preimage of a connected set to be connected

[YaelDillies]

and other simple connectedness results

---

From LTE
Co-authored-by: Kevin Buzzard k.buzzard@imperial.ac.uk

[AntoineChambert-Loir]

There is a more general theorem to prove : If a continuous map f is strict (the quotient topology on the image coincides with its topology of a subspace) and if the fibers of f are preconnected, then the preimage of a preconnected set is preconnected.

Sufficient conditions for a map to be strict are to be closed, or to be open.

An injective open map is strict, and the fibers are (sub)singletons hence are preconnected.

[YaelDillies]

That sounds significantly more advanced. Do we even have strict maps?
I think it's better to stay with this proof now and if someone comes along and proves your theorem we can shorten the already short proof of my lemmas.

[AntoineChambert-Loir]

Probably, strict maps are not in mathlib yet.
Two cases which are already worth being done are when the map is open or closed.

[jcommelin]

I changed the PR title to something that isn't strictly false 😜

@YaelDillies Could you please turn the comments by @AntoineChambert-Loir into a TODO in the code? So that someone who stumbles on them later can start an API for strict maps?

[AntoineChambert-Loir]

I changed the PR title to something that isn't strictly false 😜

Actually, @jcommelin , this was the very reason why I opened the PR and loooked at it !

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests