mathlib

a4ea8895 - 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)