Theorem ZerothHomotopy.toConnectedComponents_surjective

Modification history

2026-02-17 20:49

Mathlib/Topology/Connected/PathConnected.lean

feat(Topology/Connected/PathConnected): relate `ZerothHomotopy` and `ConnectedComponents` (#34244)

Added ZerothHomotopy.toConnectedComponents_surjective View on Github →