feat(topology/connected): make `connected_component_in` more usable, develop API (#15964)
feat(topology/connected): make `connected_component_in` more usable, develop API (#15964)

From the [Sphere Eversion Project](https://github.com/leanprover-community/sphere-eversion/blob/333231d77aa028bb164abc695ac8a4abce4af0c2/src/to_mathlib/topology/misc.lean#L516)





leanprover-community/mathlib,leanprover-community/mathlib