mathlib3

e1f01165 - feat(topology/connected): definition and basic properties about locally connected spaces (#15965)

feat(topology/connected): definition and basic properties about locally connected spaces (#15965) This was introduced in the [Sphere Eversion Project](https://github.com/leanprover-community/sphere-eversion/blob/333231d77aa028bb164abc695ac8a4abce4af0c2/src/to_mathlib/topology/misc.lean#L444); I added a clean API, proved the equivalence with "weak local connectedness" (where we don't require the bases to be made of open sets), generalized [local connectedness of normed spaces](https://github.com/leanprover-community/sphere-eversion/blob/333231d77aa028bb164abc695ac8a4abce4af0c2/src/to_mathlib/topology/misc.lean#L504) to local connectedness of locally convex spaces, and proved the lemmas @hrmacbeth asked for on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Missing.20facts.20about.20.60locally_constant.60/near/290704266).