Mathlib Map

Theorems · Definition · general topology

ZerothHomotopy.toConnectedComponents

{X : Type u_1} → [inst : TopologicalSpace X] → ZerothHomotopy X → ConnectedComponents X

The canonical map which sends a path component of X (as a term of ZerothHomotopy X) to the connected component containing it (as a term of ConnectedComponents X).

Defined in
Mathlib.Topology.Connected.PathConnected
Cited by
3 results in Mathlib
Foundations
Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
TopologicalSpace
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

connectedComponentsEquivZerothHomotopy · cited by 3connectedComponentsEquivZ…ZerothHomotopy.toConnectedComponents_apply · cited by 0ZerothHomotopy.toConnecte…ZerothHomotopy.toConnectedComponents_surjective · cited by 0ZerothHomotopy.toConnecte…coe_connectedComponentsEquivZerothHomotopy_symm · cited by 0coe_connectedComponentsEq…TopologicalSpace · cited by 24529TopologicalSpaceConnectedComponents · cited by 40ConnectedComponentsZerothHomotopy · cited by 15ZerothHomotopyQuotient.map · cited by 7Quotient.mapZerothHomotopy.toConnectedCom…CITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by4

Results whose statement or proof uses this declaration.