Commit 2026-02-17 20:49 cf8ca7bb

View on Github →

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

Estimated changes

Modified Mathlib/Data/Quot.lean

added theorem Quot.map_surjective

added theorem Quotient.map_surjective

Modified Mathlib/Topology/Connected/LocPathConnected.lean

added theorem coe_connectedComponentsEquivZerothHomotopy_symm

added theorem connectedComponentSetoid_eq_pathSetoid

added theorem connectedComponent_eq_iff_joined

added def connectedComponentsEquivZerothHomotopy

added theorem connectedComponentsEquivZerothHomotopy_apply

added theorem connectedComponentsEquivZerothHomotopy_symm_apply

Modified Mathlib/Topology/Connected/PathConnected.lean

added def ZerothHomotopy.toConnectedComponents

added theorem ZerothHomotopy.toConnectedComponents_apply

added theorem ZerothHomotopy.toConnectedComponents_surjective

added theorem biUnion_connectedComponent_pathComponent_eq