Structures · Topology
TotallyDisconnectedSpace
A space is totally disconnected if all of its connected components are singletons.
- Shape
- One type argument · adds isTotallyDisconnected_univ
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances11
- Rat
- TopCat.carrier
- CategoryTheory.Aut
- ConnectedComponents
- Ultrafilter
- Subtype
- Prod
- Sum
- Multiplicative
- Additive
- Sigma
How is a type an instance?
Loading the hierarchy index…
Assumed by83
- LightProfinite.of
- Profinite.of
- ProfiniteGrp.of
- ProfiniteAddGrp.of
- IsPreconnected.subsingleton
- ProfiniteGrp.exist_openNormalSubgroup_sub_open_nhds_of_one
- ProfiniteGrp.ofHom
- ProfiniteAddGrp.ofHom
- isTopologicalBasis_isClopen
- connectedComponent_eq_singleton
- Continuous.connectedComponentsLift
- compact_exists_isClopen_in_isOpen
- TotallyDisconnectedSpace.isTotallyDisconnected_univ
- nhds_basis_clopen
- Profinite.indexFunctor
- ProfiniteGrp.exist_openNormalAddSubgroup_sub_open_nhds_of_zero
- ContinuousMap.exists_finite_approximation_of_mem_nhds_diagonal
- Continuous.image_eq_of_connectedComponent_eq
- loc_compact_Haus_tot_disc_of_zero_dim
- subsingleton_of_preconnected_totallyDisconnected
- ContinuousMap.exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal
- AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace
- ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity
- exists_clopen_partition_of_clopen_cover
- exists_clopen_of_closed_subset_open
- ContinuousMap.exists_finite_sum_smul_approximation_of_mem_uniformity
- ContinuousMap.exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal
- Profinite.exists_lift_of_finite_of_injective_of_surjective
- Continuous.connectedComponentsLift_continuous
- Continuous.image_connectedComponent_eq_singleton
- TopologicalSpace.IsOpenCover.exists_finite_clopen_cover
- AlgebraicTopology.singularChainComplexFunctorIsoOfTotallyDisconnectedSpace
- Continuous.connectedComponentsLift_comp_coe
- ContinuousMap.denseRange_tensorHom
- TotallyDisconnectedSpace.continuousMapEquivOfConnectedSpace
- TopCat.toSSetIsoConst
- LightProfinite.of.congr_simp
- Pi.totallyDisconnectedSpace
- instTotallySeparatedSpaceOfTotallyDisconnectedSpace
- Profinite.isIso_indexCone_lift
- instTotallyDisconnectedSpaceSum
- ProfiniteGrp.hom_ofHom
- instTotallyDisconnectedSpaceSigma
- isTotallyDisconnected_of_totallyDisconnectedSpace
- Homeomorph.totallyDisconnectedSpace
- Profinite.indexCone_isLimit
- Continuous.connectedComponentsLift_unique
- LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology
- AlgebraicTopology.isZero_singularHomologyFunctor_of_totallyDisconnectedSpace
- Subtype.totallyDisconnectedSpace
Ancestors0
No ancestors.