Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes