TotallyDisconnected

📁 Source: Mathlib/Topology/Connected/TotallyDisconnected.lean

Statistics

Metric	Count
Definitions connectedComponentsLift, connectedComponentsMap, IsTotallyDisconnected, IsTotallySeparated, TotallyDisconnectedSpace, continuousMapEquivOfConnectedSpace, TotallySeparatedSpace	7
Theorems totallyDisconnectedSpace, connectedComponentsLift_apply_coe, connectedComponentsLift_comp_coe, connectedComponentsLift_continuous, connectedComponentsLift_unique, connectedComponentsMap_continuous, image_connectedComponent_eq_singleton, image_eq_of_connectedComponent_eq, constant, constant_of_mapsTo, eqOn_const_of_mapsTo, subsingleton, isTotallyDisconnected, totallyDisconnectedSpace, constant, totallyDisconnectedSpace, totallyDisconnectedSpace, isTotallyDisconnected, isTotallyDisconnected_image, isTotallyDisconnected_range, continuousMapEquivOfConnectedSpace_symm_apply_apply, eq_of_continuous, isTotallyDisconnected_univ, isTotallySeparated_univ, of_discrete, totallyDisconnectedSpace, connectedComponent_eq_singleton, connectedComponents_lift_unique', exists_isClopen_of_totally_separated, instTotallyDisconnectedSpaceAdditive, instTotallyDisconnectedSpaceMultiplicative, instTotallyDisconnectedSpaceSigma, instTotallyDisconnectedSpaceSum, isTotallyDisconnected_empty, isTotallyDisconnected_of_image, isTotallyDisconnected_of_isTotallySeparated, isTotallyDisconnected_of_totallyDisconnectedSpace, isTotallyDisconnected_singleton, isTotallySeparated_empty, isTotallySeparated_singleton, totallyDisconnectedSpace_iff, totallyDisconnectedSpace_iff_connectedComponent_singleton, totallyDisconnectedSpace_iff_connectedComponent_subsingleton, totallyDisconnectedSpace_subtype_iff, totallySeparatedSpace_iff, totallySeparatedSpace_iff_exists_isClopen	46
Total	53

ConnectedComponents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyDisconnectedSpace 📖	mathematical	—	TotallyDisconnectedSpace ConnectedComponents instTopologicalSpace	—	totallyDisconnectedSpace_iff_connectedComponent_singleton Function.Surjective.forall surjective_coe Topology.IsQuotientMap.image_connectedComponent isQuotientMap_coe connectedComponents_preimage_singleton isConnected_connectedComponent Set.image_preimage_eq

Continuous

Definitions

Name	Category	Theorems
connectedComponentsLift 📖	CompOp	4 math math: connectedComponentsLift_comp_coe, connectedComponentsLift_unique, connectedComponentsLift_continuous, connectedComponentsLift_apply_coe
connectedComponentsMap 📖	CompOp	1 math math: connectedComponentsMap_continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connectedComponentsLift_apply_coe 📖	mathematical	Continuous	connectedComponentsLift	—	—
connectedComponentsLift_comp_coe 📖	mathematical	Continuous	ConnectedComponents connectedComponentsLift	—	—
connectedComponentsLift_continuous 📖	mathematical	Continuous	ConnectedComponents ConnectedComponents.instTopologicalSpace connectedComponentsLift	—	quotient_liftOn' image_eq_of_connectedComponent_eq
connectedComponentsLift_unique 📖	mathematical	Continuous ConnectedComponents	connectedComponentsLift	—	connectedComponents_lift_unique' connectedComponentsLift_comp_coe
connectedComponentsMap_continuous 📖	mathematical	Continuous	ConnectedComponents ConnectedComponents.instTopologicalSpace connectedComponentsMap	—	connectedComponentsLift_continuous ConnectedComponents.totallyDisconnectedSpace comp ConnectedComponents.continuous_coe
image_connectedComponent_eq_singleton 📖	mathematical	Continuous	Set.image connectedComponent Set Set.instSingletonSet	—	Set.subsingleton_iff_singleton Set.mem_image_of_mem mem_connectedComponent IsPreconnected.subsingleton IsPreconnected.image isPreconnected_connectedComponent continuousOn
image_eq_of_connectedComponent_eq 📖	—	Continuous connectedComponent	—	—	Set.singleton_eq_singleton_iff image_connectedComponent_eq_singleton

IsPreconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constant 📖	—	IsPreconnected ContinuousOn Set Set.instMembership	—	—	subsingleton TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete image Set.mem_image_of_mem
constant_of_mapsTo 📖	—	IsPreconnected IsDiscrete ContinuousOn Set.MapsTo Set Set.instMembership	—	—	PreconnectedSpace.constant isDiscrete_iff_discreteTopology isPreconnected_iff_preconnectedSpace ContinuousOn.mapsToRestrict
eqOn_const_of_mapsTo 📖	mathematical	IsPreconnected IsDiscrete ContinuousOn Set.MapsTo Set.Nonempty	Set Set.instMembership Set.EqOn	—	Set.eq_empty_or_nonempty Set.eqOn_empty constant_of_mapsTo
subsingleton 📖	mathematical	IsPreconnected	Set.Subsingleton	—	TotallyDisconnectedSpace.isTotallyDisconnected_univ Set.subset_univ

IsTotallySeparated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTotallyDisconnected 📖	mathematical	IsTotallySeparated	IsTotallyDisconnected	—	isTotallyDisconnected_of_isTotallySeparated

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyDisconnectedSpace 📖	mathematical	TotallyDisconnectedSpace	topologicalSpace	—	IsPreconnected.image Continuous.continuousOn continuous_apply IsPreconnected.subsingleton

PreconnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
constant 📖	—	Continuous	—	—	IsPreconnected.constant isPreconnected_univ Continuous.continuousOn

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyDisconnectedSpace 📖	mathematical	—	TotallyDisconnectedSpace instTopologicalSpaceProd	—	IsPreconnected.image Continuous.continuousOn continuous_fst continuous_snd IsPreconnected.subsingleton

Subtype

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
totallyDisconnectedSpace 📖	mathematical	—	TotallyDisconnectedSpace instTopologicalSpaceSubtype	—	totallyDisconnectedSpace_subtype_iff isTotallyDisconnected_of_totallyDisconnectedSpace

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTotallyDisconnected 📖	—	Topology.IsEmbedding IsTotallyDisconnected Set.image	—	—	isTotallyDisconnected_of_image Continuous.continuousOn continuous injective
isTotallyDisconnected_image 📖	mathematical	Topology.IsEmbedding	IsTotallyDisconnected Set.image	—	isTotallyDisconnected Set.inter_subset_right Set.image_preimage_inter Set.inter_eq_left Set.Subsingleton.image Topology.IsInducing.isPreconnected_image isInducing
isTotallyDisconnected_range 📖	mathematical	Topology.IsEmbedding	IsTotallyDisconnected Set.range TotallyDisconnectedSpace	—	totallyDisconnectedSpace_iff Set.image_univ isTotallyDisconnected_image

TotallyDisconnectedSpace

Definitions

Name	Category	Theorems
continuousMapEquivOfConnectedSpace 📖	CompOp	1 math math: continuousMapEquivOfConnectedSpace_symm_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousMapEquivOfConnectedSpace_symm_apply_apply 📖	mathematical	—	DFunLike.coe ContinuousMap ContinuousMap.instFunLike Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm continuousMapEquivOfConnectedSpace	—	—
eq_of_continuous 📖	—	Continuous	—	—	IsPreconnected.subsingleton IsPreconnected.image PreconnectedSpace.isPreconnected_univ Continuous.continuousOn
isTotallyDisconnected_univ 📖	mathematical	—	IsTotallyDisconnected Set.univ	—	—

TotallySeparatedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTotallySeparated_univ 📖	mathematical	—	IsTotallySeparated Set.univ	—	—
of_discrete 📖	mathematical	—	TotallySeparatedSpace	—	isOpen_discrete Eq.subset Set.instReflSubset Set.compl_union_self disjoint_compl_left
totallyDisconnectedSpace 📖	mathematical	—	TotallyDisconnectedSpace	—	IsTotallySeparated.isTotallyDisconnected isTotallySeparated_univ

(root)

Definitions

Name	Category	Theorems
IsTotallyDisconnected 📖	MathDef	12 math math: totallyDisconnectedSpace_subtype_iff, IsTotallySeparated.isTotallyDisconnected, isTotallyDisconnected_of_totallyDisconnectedSpace, isTotallyDisconnected_iff_lt, isTotallyDisconnected_singleton, Set.Countable.isTotallyDisconnected, Topology.IsEmbedding.isTotallyDisconnected_range, isTotallyDisconnected_of_isTotallySeparated, Topology.IsEmbedding.isTotallyDisconnected_image, TotallyDisconnectedSpace.isTotallyDisconnected_univ, isTotallyDisconnected_empty, totallyDisconnectedSpace_iff
IsTotallySeparated 📖	MathDef	5 math math: isTotallySeparated_singleton, isTotallySeparated_empty, krullTopology_isTotallySeparated, TotallySeparatedSpace.isTotallySeparated_univ, totallySeparatedSpace_iff
TotallyDisconnectedSpace 📖	CompData	265 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightProfinite.proj_comp_transitionMap, LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, LightCondensed.isoFinYonedaComponents_hom_apply, ProfiniteGrp.coe_of, ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, LightCondensed.ihomPoints_apply, Profinite.Extend.cocone_pt, CondensedMod.IsSolid.isIso_solidification_map, Profinite.forget_preservesLimits, instFullFintypeCatProfiniteToProfinite, LightCondensed.forget_obj_val_map, Profinite.Extend.functorOp_map, ProfiniteGrp.limit_one_val, ProfiniteAddGrp.ofHom_hom, LightCondensed.ihomPoints_symm_comp, Profinite.instEnoughProjectives, ProfiniteGrp.ProfiniteCompletion.lift_eta, LightCondSet.continuous_coinducingCoprod, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, totallyDisconnectedSpace_iff_connectedComponent_singleton, LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, LightCondensed.isoFinYoneda_inv_app, CondensedMod.isDiscrete_tfae, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, Profinite.Extend.cone_π_app, instFaithfulFintypeCatLightProfiniteToLightProfinite, ProfiniteAddGrp.ofHom_apply, LightCondensed.finYoneda_map, ProfiniteGrp.coe_id, Profinite.effectiveEpi_tfae, LightCondMod.isDiscrete_tfae, LocallyConstant.freeOfProfinite, instFaithfulLightDiagramProfiniteLightDiagramToProfinite, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, CategoryTheory.PreGaloisCategory.instTotallyDisconnectedSpaceAutFunctorFintypeCat, LightCondensed.discrete_map, LightProfinite.proj_comp_transitionMapLE', lightDiagramToProfinite_map, LightProfinite.Extend.cocone_ι_app, totallyDisconnectedSpace_subtype_iff, ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Condensed.lanPresheafExt_inv, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, instFaithfulFintypeCatProfiniteToProfinite, Profinite.injective_of_light, LightCondSet.topCatAdjunctionUnit_val_app_apply, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Profinite.epi_iff_surjective, lightProfiniteToLightDiagram_map, Profinite.exists_locallyConstant_finite_aux, Prod.totallyDisconnectedSpace, Profinite.instTotallyDisconnectedSpaceCarrierToTop, ProfiniteGrp.toLimit_surjective, LightProfinite.isClosedMap, ProfiniteAddGrp.hom_neg_apply, lightDiagramToLightProfinite_obj, Condensed.isoFinYonedaComponents_hom_apply, ProfiniteGrp.hom_id, ProfiniteAddGrp.hom_id, Profinite.Extend.functorOp_obj, ProfiniteAddGrp.neg_hom_apply, instTotallyDisconnectedSpaceMultiplicative, Condensed.finYoneda_map, LightProfinite.lightToProfinite_map_proj_eq, FintypeCat.toProfinite_map_hom_hom_apply, ProfiniteGrp.denseRange_toLimit, Profinite.hasColimits, ProfiniteAddGrp.limit_zero_val, ProfiniteGrp.comp_apply, LightProfinite.effectiveEpi_iff_surjective, ProfiniteAddGrp.coe_of, ProfiniteAddGrp.comp_apply, LightProfinite.continuous_iff_convergent, Profinite.instPreregular, LightCondensed.internallyProjective_iff_tensor_condition, LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite, instTotallyDisconnectedSpaceSum, LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, LightProfinite.instCountableDiscreteQuotient, ProfiniteGrp.ofHom_hom, Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite, ProfiniteGrp.topologicalGroup, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.hasSheafify, ProfiniteGrp.hom_comp, InfiniteGalois.mulEquivToLimit_symm_continuous, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightProfinite.instWEqualsLocallyBijectiveCoherentTopology, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, ProfiniteGrp.inv_hom_apply, ProfiniteAddGrp.id_apply, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, Condensed.instPreservesFiniteProductsOppositeProfiniteVal, ProfiniteGrp.cone_pt, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.isoFinYonedaComponents_inv_comp, ProfiniteAddGrp.coe_id, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone, instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, InfiniteGalois.proj_adjoin_singleton_val, Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier, LightProfinite.Extend.functor_map, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier, ProfiniteGrp.limit_mul_val, ProfiniteGrp.ProfiniteCompletion.denseRange, LightCondensed.forget_map_val_app, LightCondensed.isoLocallyConstantOfIsColimit_inv, Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus, FintypeCat.toLightProfinite_map_hom_hom_apply, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus, LightProfinite.injective, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, Profinite.projective_ultrafilter, CompHaus.toProfinite_obj', instTotallyDisconnectedSpaceUltrafilter, Condensed.isoLocallyConstantOfIsColimit_inv, Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus, lightDiagramToProfinite_obj, ProfiniteAddGrp.limit_add_val, Condensed.lanPresheafNatIso_hom_app, LightProfinite.surjective_transitionMapLE, Profinite.Extend.functor_obj, LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, LightCondensed.free_internallyProjective_iff_tensor_condition', ProfiniteGrp.profiniteCompletion_map, LightProfinite.instHasCountableLimits, LightProfinite.forget_reflectsIsomorphisms, Condensed.isoFinYonedaComponents_inv_comp, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, ProfiniteAddGrp.limit_ext_iff, Profinite.lift_lifts_assoc, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, LightProfinite.Extend.functorOp_map, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology, ProfiniteGrp.hom_inv_apply, instEssentiallySmallLightProfinite, LightCondensed.hom_ext_iff, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, loc_compact_t2_tot_disc_iff_tot_sep, ProfiniteGrp.cone_π_app, LightCondensed.underlying_obj, LightCondSet.hom_naturality_apply, CondensedSet.isDiscrete_tfae, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, Profinite.exists_locallyConstant, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, Profinite.lift_lifts, LightCondensed.equalizerCondition, InfiniteGalois.toAlgEquivAux_eq_liftNormal, LightCondMod.hom_naturality_apply, TotallySeparatedSpace.totallyDisconnectedSpace, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite, ProfiniteGrp.toLimit_injective, lightProfiniteToLightDiagram_obj, Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite, ProfiniteAddGrp.coe_comp, LightDiagram.id_hom_hom_hom_apply, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightCondensed.lanPresheafNatIso_hom_app, ProfiniteGrp.ofHom_apply, Topology.IsEmbedding.isTotallyDisconnected_range, lightCondSetToTopCat_obj_carrier, instTotallyDisconnectedSpaceAdditive, LightProfinite.Extend.cocone_pt, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier, ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, LightCondensed.ihom_map_val_app, Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite, Profinite.Extend.cocone_ι_app, Homeomorph.totallyDisconnectedSpace, Condensed.isoFinYoneda_hom_app, Profinite.Extend.cone_pt, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, lightDiagramToLightProfinite_map, LightProfinite.surjective_transitionMap, ProfiniteGrp.coe_comp, Profinite.projective_of_extrDisc, LightCondensed.lanPresheafExt_inv, LightProfinite.epi_iff_surjective, Condensed.lanPresheafExt_hom, instFullLightDiagramProfiniteLightDiagramToProfinite, Profinite.injective_of_finite, InfiniteGalois.mk_toAlgEquivAux, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, InfiniteGalois.proj_of_le, Stonean.instProjectiveProfiniteObjToProfinite, LightCondSet.isDiscrete_tfae, LightCondSet.topCatAdjunctionUnit_val_app, LightDiagram.comp_hom_hom_hom_apply, Profinite.presentation.epi_π, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.instPreregular, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, ProfiniteGrp.toLimitFun_continuous, ProfiniteGrp.diagram_map, LightCondensed.id_val, InfiniteGalois.algEquivToLimit_continuous, totallyDisconnectedSpace_iff_connectedComponent_subsingleton, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, ProfiniteGrp.id_apply, Profinite.Nobeling.isClosedEmbedding, LightProfinite.proj_surjective, LightProfinite.proj_comp_transitionMapLE, LightProfinite.instEpiAppOppositeNatπAsLimitCone, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, ProfiniteGrp.isIso_toLimit, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, InfiniteGalois.limitToAlgEquiv_symm_apply, LightCondensed.internallyProjective_iff_tensor_condition', LightProfinite.hasSheafify_type, LightCondensed.comp_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, LightCondensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, Subtype.totallyDisconnectedSpace, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, LightCondSet.toTopCatMap_hom_apply, LightCondensed.lanPresheafExt_hom, Rat.instTotallyDisconnectedSpace, Profinite.exists_locallyConstant_finite_nonempty, Profinite.hasLimits, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Condensed.isoFinYoneda_inv_app, ProfiniteGrp.limit_ext_iff, Profinite.exists_locallyConstant_fin_two, ProfiniteAddGrp.hom_comp, Profinite.effectiveEpiFamily_tfae, LightProfinite.proj_comp_transitionMap', totallyDisconnectedSpace_iff, ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, Profinite.Extend.functor_map, Condensed.locallyConstantIsoFinYoneda_hom_app, ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, instFullFintypeCatLightProfiniteToLightProfinite, Condensed.equalizerCondition_profinite, Profinite.instHasPropTotallyDisconnectedSpaceCarrier, Profinite.isIso_asLimitCone_lift, Condensed.lanPresheafIso_hom, ProfiniteAddGrp.topologicalAddGroup, ConnectedComponents.totallyDisconnectedSpace, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal, Profinite.exists_hom, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology, ProfiniteGrp.diagram_obj, ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite
TotallySeparatedSpace 📖	CompData	19 math math: CompletelyRegularSpace.totallySeparatedSpace_of_cardinalMk_lt_continuum, PriestleySpace.toTotallySeparatedSpace, instTotallySeparatedSpaceOfT2SpaceOfPrespectralSpace, instTotallySeparatedSpaceAlgEquivOfIsIntegral, NonarchimedeanAddGroup.instTotallySeparated, CompleteType.instTotallySeparatedSpaceCompleteType, instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space, TotallySeparatedSpace.of_discrete, loc_compact_t2_tot_disc_iff_tot_sep, totallySeparatedSpace_iff, totallySeparatedSpace_of_t0_of_basis_clopen, instTotallySeparatedSpaceOfIsUltrametricDist, OnePoint.instTotallySeparatedSpaceOfDiscreteTopology, Set.Countable.totallySeparatedSpace, totallySeparatedSpace_iff_exists_isClopen, totallySeparatedSpace_of_t1_of_basis_clopen, CompletelyRegularSpace.instTotallySeparatedSpaceOfCountable, NonarchimedeanGroup.instTotallySeparated, instTotallySeparatedSpaceOfTotallyDisconnectedSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
connectedComponent_eq_singleton 📖	mathematical	—	connectedComponent Set Set.instSingletonSet	—	totallyDisconnectedSpace_iff_connectedComponent_singleton
connectedComponents_lift_unique' 📖	—	ConnectedComponents	—	—	Function.Surjective.injective_comp_right ConnectedComponents.surjective_coe
exists_isClopen_of_totally_separated 📖	mathematical	—	Pairwise Set IsClopen Set.instMembership Compl.compl Set.instCompl	—	totallySeparatedSpace_iff_exists_isClopen
instTotallyDisconnectedSpaceAdditive 📖	mathematical	—	TotallyDisconnectedSpace Additive instTopologicalSpaceAdditive	—	—
instTotallyDisconnectedSpaceMultiplicative 📖	mathematical	—	TotallyDisconnectedSpace Multiplicative instTopologicalSpaceMultiplicative	—	—
instTotallyDisconnectedSpaceSigma 📖	mathematical	TotallyDisconnectedSpace	instTopologicalSpaceSigma	—	Set.eq_empty_or_nonempty Set.subsingleton_empty Sigma.isConnected_iff Set.Subsingleton.image IsPreconnected.subsingleton IsConnected.isPreconnected
instTotallyDisconnectedSpaceSum 📖	mathematical	—	TotallyDisconnectedSpace instTopologicalSpaceSum	—	Sum.isPreconnected_iff Set.Subsingleton.image IsPreconnected.subsingleton
isTotallyDisconnected_empty 📖	mathematical	—	IsTotallyDisconnected Set Set.instEmptyCollection	—	—
isTotallyDisconnected_of_image 📖	—	ContinuousOn IsTotallyDisconnected Set.image	—	—	Set.image_mono IsPreconnected.image ContinuousOn.mono Set.mem_image_of_mem
isTotallyDisconnected_of_isTotallySeparated 📖	mathematical	IsTotallySeparated	IsTotallyDisconnected	—	Set.Nonempty.ne_empty HasSubset.Subset.trans Set.instIsTransSubset Disjoint.inter_eq Set.inter_empty
isTotallyDisconnected_of_totallyDisconnectedSpace 📖	mathematical	—	IsTotallyDisconnected	—	TotallyDisconnectedSpace.isTotallyDisconnected_univ Set.subset_univ
isTotallyDisconnected_singleton 📖	mathematical	—	IsTotallyDisconnected Set Set.instSingletonSet	—	Set.Subsingleton.anti Set.subsingleton_singleton
isTotallySeparated_empty 📖	mathematical	—	IsTotallySeparated Set Set.instEmptyCollection	—	—
isTotallySeparated_singleton 📖	mathematical	—	IsTotallySeparated Set Set.instSingletonSet	—	Set.eq_of_mem_singleton
totallyDisconnectedSpace_iff 📖	mathematical	—	TotallyDisconnectedSpace IsTotallyDisconnected Set.univ	—	—
totallyDisconnectedSpace_iff_connectedComponent_singleton 📖	mathematical	—	TotallyDisconnectedSpace connectedComponent Set Set.instSingletonSet	—	totallyDisconnectedSpace_iff_connectedComponent_subsingleton Set.subsingleton_iff_singleton mem_connectedComponent
totallyDisconnectedSpace_iff_connectedComponent_subsingleton 📖	mathematical	—	TotallyDisconnectedSpace Set.Subsingleton connectedComponent	—	TotallyDisconnectedSpace.isTotallyDisconnected_univ Set.subset_univ isPreconnected_connectedComponent Set.eq_empty_or_nonempty Set.subsingleton_empty Set.Subsingleton.anti IsPreconnected.subset_connectedComponent
totallyDisconnectedSpace_subtype_iff 📖	mathematical	—	TotallyDisconnectedSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership IsTotallyDisconnected	—	Topology.IsEmbedding.isTotallyDisconnected_range Topology.IsEmbedding.subtypeVal Subtype.range_val
totallySeparatedSpace_iff 📖	mathematical	—	TotallySeparatedSpace IsTotallySeparated Set.univ	—	—
totallySeparatedSpace_iff_exists_isClopen 📖	mathematical	—	TotallySeparatedSpace Pairwise Set IsClopen Set.instMembership Compl.compl Set.instCompl	—	isClopen_of_disjoint_cover_open Set.disjoint_iff IsClopen.compl Eq.ge Set.union_compl_self disjoint_compl_right

---

← Back to Index