Theorems · Definition · general topology
ConnectedComponents
(α : Type u) → [TopologicalSpace α] → Type u
The quotient of a space by its connected components
- Defined in
- Mathlib.Topology.Connected.Clopen
- Cited by
- 40 results in Mathlib
- Foundations
- Depth 11 from the axioms · uses no axioms
- Assumes
- TopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- connectedComponentSetoidproof · cited by 4
Cited by51
Results whose statement or proof uses this declaration.
- ConnectedComponents.mkstatement · cited by 25
- ConnectedComponents.surjective_coestatement · cited by 8
- Continuous.connectedComponentsMapstatement · cited by 7
- ConnectedComponents.equivOfIsClopenstatement and proof · cited by 5
- Continuous.connectedComponentsLiftstatement and proof · cited by 4
- ZerothHomotopy.toConnectedComponentsstatement · cited by 3
- connectedComponentsEquivZerothHomotopystatement · cited by 3
- ConnectedComponents.continuous_coestatement · cited by 3
- ConnectedComponents.isQuotientMap_coestatement · cited by 3
- Topology.IsCoinducing.connectedComponentsHomeomorphstatement · cited by 3
- ConnectedComponents.coe_eq_coestatement · cited by 2
- connectedComponents_preimage_singletonstatement · cited by 2