mathlib3

2961e79c - feat(topology/connected.lean): define pi_0 and prove basic properties (#6188)

feat(topology/connected.lean): define pi_0 and prove basic properties (#6188) Define and prove basic properties of pi_0, the functor quotienting a space by its connected components. For dot notation convenience, this PR renames `subset_connected_component` to `is_preconnected.subset_connected_component` and also defines the weaker version `is_connected.subset_connected_component`. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>