# Commit 2021-02-16 09:30 2961e79c

View on Github →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`

.