Basic

📁 Source: Mathlib/Topology/Category/CompHausLike/Basic.lean

Statistics

Metric	Count
Definitions CompHausLike, HasProp, category, compHausLikeToTop, concreteCategory, const, fullyFaithfulCompHausLikeToTop, fullyFaithfulToCompHausLike, hasForget₂, homeoOfIso, instCoeSortType, isoEquivHomeo, isoOfBijective, isoOfHomeo, of, ofHom, toCompHausLike, toTop	18
Theorems hasProp, coe_comp, coe_id, coe_of, compHausLikeToTop_map, const_comp, epi_of_surjective, forget_reflectsIsomorphisms, hom_ofHom, homeoOfIso_apply, homeoOfIso_symm_apply, instCompactSpaceCarrierObjTopCatCompHausLikeToTop, instFaithfulToCompHausLike, instFaithfulTopCatCompHausLikeToTop, instFullToCompHausLike, instFullTopCatCompHausLikeToTop, instHasPropCarrierToTop, instT2SpaceCarrierObjTopCatCompHausLikeToTop, isClosedMap, isIso_of_bijective, is_compact, is_hausdorff, isoEquivHomeo_apply, isoEquivHomeo_symm_apply, isoOfHomeo_hom_hom_hom_apply, isoOfHomeo_inv_hom_hom_apply, mono_iff_injective, ofHom_comp, ofHom_id, prop, toCompHausLike_map	31
Total	49

CompHausLike

Definitions

Name	Category	Theorems
HasProp 📖	CompData	6 math math: CompHaus.instHasPropTrue, instHasPropCarrierToTop, Stonean.instHasPropExtremallyDisconnectedCarrier, LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology, LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop, Profinite.instHasPropTotallyDisconnectedSpaceCarrier
category 📖	CompOp	309 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightProfinite.proj_comp_transitionMap, LightProfinite.Extend.functorOp_obj, LightCondensed.lanPresheafIso_hom, instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts, LightCondensed.isoFinYonedaComponents_hom_apply, ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, LightCondensed.ihomPoints_apply, instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions, Profinite.Extend.cocone_pt, condensedSetToTopCat_obj_carrier, CondensedMod.IsSolid.isIso_solidification_map, Profinite.forget_preservesLimits, Condensed.hom_ext_iff, instFullFintypeCatProfiniteToProfinite, LightCondensed.forget_obj_val_map, Stonean.instProjective, Profinite.Extend.functorOp_map, instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions, LightCondensed.ihomPoints_symm_comp, pullback.condition, Profinite.instEnoughProjectives, LightCondSet.continuous_coinducingCoprod, LightCondSet.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.isoFinYoneda_inv_app, CondensedMod.isDiscrete_tfae, coe_id, finiteCoproduct.ι_desc, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, CondensedSet.hom_naturality_apply, LocallyConstantModule.functorToPresheaves_obj_obj_isModule, Profinite.Extend.cone_π_app, instFaithfulFintypeCatLightProfiniteToLightProfinite, LightCondensed.finYoneda_map, CondensedMod.LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, Condensed.discrete_map, HasExplicitPullbacksOfInclusions.hasProp, Profinite.effectiveEpi_tfae, Stonean.instEffectivelyEnoughCompHausToCompHaus, LightCondMod.isDiscrete_tfae, instFaithfulLightDiagramProfiniteLightDiagramToProfinite, instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet, CondensedMod.LocallyConstant.instFaithfulModuleCatCondensedDiscrete, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, LightCondensed.discrete_map, pullback.isLimit_lift, LightProfinite.proj_comp_transitionMapLE', lightDiagramToProfinite_map, CompHaus.hasColimits, LightProfinite.Extend.cocone_ι_app, ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Condensed.lanPresheafExt_inv, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, compactumToCompHaus.full, instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed, instFaithfulFintypeCatProfiniteToProfinite, Profinite.injective_of_light, CompHaus.instEnoughProjectives, LightCondSet.topCatAdjunctionUnit_val_app_apply, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Profinite.epi_iff_surjective, lightProfiniteToLightDiagram_map, Profinite.exists_locallyConstant_finite_aux, instFullCompHausCondensedTypeCompHausToCondensed', LightProfinite.isClosedMap, compactumToCompHaus.essSurj, lightDiagramToLightProfinite_obj, Profinite.isIso_indexCone_lift, LocallyConstant.counitApp_app, Condensed.isoFinYonedaComponents_hom_apply, LocallyConstantModule.functorToPresheaves_map_app, Condensed.instPreservesFiniteProductsOppositeCompHausVal, Profinite.Extend.functorOp_obj, homeoOfIso_symm_apply, Condensed.finYoneda_map, LightProfinite.lightToProfinite_map_proj_eq, instFullTopCatCompHausLikeToTop, LocallyConstant.incl_of_counitAppApp, isClosedMap, sigmaComparison_eq_comp_isos, FintypeCat.toProfinite_map_hom_hom_apply, Profinite.hasColimits, CondensedMod.isDiscrete_iff_isDiscrete_forget, isoEquivHomeo_symm_apply, LightProfinite.effectiveEpi_iff_surjective, compactumToCompHaus.isEquivalence, Stonean.effectiveEpiFamily_tfae, CondensedMod.LocallyConstant.instFullModuleCatCondensedDiscrete, instFullCompHausCondensedSetCompHausToCondensed, Profinite.instPreregular, LightCondensed.internallyProjective_iff_tensor_condition, LightProfinite.instPreservesEpimorphismsProfiniteLightToProfinite, LightProfinite.instCountableDiscreteQuotient, Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite, finiteCoproduct.isOpenEmbedding_ι, Sigma.isOpenEmbedding_ι, CompHaus.lift_lifts, instPreservesFiniteLimitsLightProfiniteLightCondSetLightProfiniteToLightCondSet, LightProfinite.hasSheafify, CondensedMod.epi_iff_surjective_on_stonean, LightCondMod.LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, Stonean.epi_iff_surjective, instFaithfulTopCatCompHausLikeToTop, LightProfinite.instWEqualsLocallyBijectiveCoherentTopology, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, CondensedSet.epi_iff_surjective_on_stonean, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, Stonean.instPreregular, instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions, Condensed.instPreservesFiniteProductsOppositeProfiniteVal, instPreservesLimitsOfShapeLightProfiniteLightCondSetLightProfiniteToLightCondSetOfCountableCategory, LightCondensed.isoFinYonedaComponents_inv_comp, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', LocallyConstant.functorToPresheaves_map_app, CondensedSet.topCatAdjunctionUnit_val_app_apply, Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone, instFaithfulLightProfiniteLightCondSetLightProfiniteToLightCondSet, compactumToCompHaus.faithful, LightProfinite.Extend.functor_map, ofHom_id, LightCondensed.instPreservesLimitsOfShapeOppositeLightProfiniteDiscreteCarrier, instT2SpaceCarrierObjTopCatCompHausLikeToTop, ofHom_comp, LightCondensed.forget_map_val_app, LightCondensed.isoLocallyConstantOfIsColimit_inv, Condensed.comp_val, Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus, CondensedMod.hom_naturality_apply, FintypeCat.toLightProfinite_map_hom_hom_apply, Condensed.instIsRightKanExtensionFintypeCatCondensedModProfiniteProfiniteSolidProfiniteSolidCounit, instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus, Stonean.forget.preservesLimits, Condensed.epi_iff_locallySurjective_on_compHaus, LightProfinite.injective, LightCondensed.isLocallySurjective_iff_locallySurjective_on_lightProfinite, Profinite.projective_ultrafilter, CompHaus.toProfinite_obj', Condensed.isoLocallyConstantOfIsColimit_inv, Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus, lightDiagramToProfinite_obj, instHasPullbacksOfHasExplicitPullbacks, Condensed.lanPresheafNatIso_hom_app, LightProfinite.surjective_transitionMapLE, Profinite.Extend.functor_obj, instHasCoproduct, mono_iff_injective, finiteCoproduct.ι_desc_assoc, LocallyConstantModule.functorToPresheaves_obj_map, LightCondensed.free_internallyProjective_iff_tensor_condition', LightProfinite.instHasCountableLimits, LightProfinite.forget_reflectsIsomorphisms, forget_reflectsIsomorphisms, Condensed.isoFinYonedaComponents_inv_comp, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, CondensedSet.continuous_coinducingCoprod, Profinite.lift_lifts_assoc, instIsEquivalenceLightDiagramLightProfiniteLightDiagramToLightProfinite, CompHausOpToFrame.faithful, CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, LightProfinite.Extend.functorOp_map, instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop, instEssentiallySmallLightProfinite, CondensedSet.topCatAdjunctionUnit_val_app, LightCondensed.hom_ext_iff, LocallyConstantModule.functorToPresheaves_obj_obj_carrier, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, pullback.condition_assoc, pullback.cone_π, LightCondensed.underlying_obj, const_comp, CompHaus.instPreregular, finiteCoproduct.ι_injective, LightCondSet.hom_naturality_apply, CompHaus.lift_lifts_assoc, CondensedSet.isDiscrete_tfae, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, Profinite.exists_locallyConstant, CompHaus.effectiveEpi_tfae, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, Profinite.lift_lifts, LightCondensed.equalizerCondition, LightCondMod.hom_naturality_apply, homeoOfIso_apply, LightCondensed.ihomPoints_symm_apply, LightCondensed.discrete_obj, CondensedMod.LocallyConstant.instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete, Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite, lightProfiniteToLightDiagram_obj, Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite, LightDiagram.id_hom_hom_hom_apply, LightCondMod.LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, LightCondensed.lanPresheafNatIso_hom_app, instFaithfulCompHausCondensedTypeCompHausToCondensed', lightCondSetToTopCat_obj_carrier, CompHaus.presentation.epi_π, instHasLimitWalkingCospanCospan, compHausLikeToTop_map, CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete, LightProfinite.Extend.cocone_pt, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus, instPreservesFiniteCoproductsToCompHausLike, toCompHausLike_map, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, isIsoSigmaComparison, Condensed.instPreservesFiniteProductsOppositeStoneanVal, CompHaus.hasLimits, Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite, Profinite.Extend.cocone_ι_app, CondensedMod.epi_iff_locallySurjective_on_compHaus, CompHaus.projective_ultrafilter, Stonean.instReflectsEffectiveEpisCompHausToCompHaus, Condensed.isoFinYoneda_hom_app, Profinite.Extend.cone_pt, instFullLightProfiniteLightCondSetLightProfiniteToLightCondSet, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, lightDiagramToLightProfinite_map, LightProfinite.surjective_transitionMap, CompHaus.epi_iff_surjective, Profinite.projective_of_extrDisc, LightCondensed.lanPresheafExt_inv, LightProfinite.epi_iff_surjective, Condensed.lanPresheafExt_hom, instFullLightDiagramProfiniteLightDiagramToProfinite, Profinite.injective_of_finite, instFaithfulCompHausCondensedSetCompHausToCondensed, Stonean.instProjectiveCompHausCompHaus, CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf, isoOfHomeo_inv_hom_hom_apply, CompHaus.Gleason, LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, hom_ofHom, instFullToCompHausLike, LocallyConstant.sigmaComparison_comp_sigmaIso, Stonean.instProjectiveProfiniteObjToProfinite, instPreservesLimitWalkingCospanCospanToCompHausLike, LightCondSet.isDiscrete_tfae, LightCondSet.topCatAdjunctionUnit_val_app, LightDiagram.comp_hom_hom_hom_apply, Profinite.presentation.epi_π, LightCondensed.instFinalNatCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteOpPtAsLimitConeFunctorOp, LightProfinite.instPreregular, LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, Condensed.underlying_obj, LightCondensed.id_val, LocallyConstant.incl_comap, LightProfinite.Extend.functor_obj, LightCondensed.isoFinYoneda_hom_app, LightProfinite.proj_surjective, LightProfinite.proj_comp_transitionMapLE, LightProfinite.instEpiAppOppositeNatπAsLimitCone, isoEquivHomeo_apply, LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, finitaryExtensive, LightCondensed.instHasColimitsOfShapeCostructuredArrowOppositeFintypeCatLightProfiniteOpToLightProfiniteType, CondensedSet.toTopCatMap_hom_apply, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, LightCondensed.internallyProjective_iff_tensor_condition', LightProfinite.hasSheafify_type, LightCondensed.comp_val, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, instCompactSpaceCarrierObjTopCatCompHausLikeToTop, isoOfHomeo_hom_hom_hom_apply, LightCondensed.underlying_map, Condensed.underlying_map, LightCondMod.isDiscrete_iff_isDiscrete_forget, instIsEquivalenceLightProfiniteLightDiagramLightProfiniteToLightDiagram, LightCondSet.toTopCatMap_hom_apply, CompHaus.effectiveEpiFamily_tfae, CondensedSet.epi_iff_locallySurjective_on_compHaus, instFaithfulToCompHausLike, LightCondensed.lanPresheafExt_hom, Profinite.exists_locallyConstant_finite_nonempty, Profinite.hasLimits, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Condensed.isoFinYoneda_inv_app, CondensedMod.LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, Profinite.exists_locallyConstant_fin_two, Profinite.effectiveEpiFamily_tfae, LightProfinite.proj_comp_transitionMap', ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, Profinite.Extend.functor_map, Condensed.id_val, Stonean.instPreservesEffectiveEpisCompHausToCompHaus, Condensed.locallyConstantIsoFinYoneda_hom_app, LocallyConstantModule.functorToPresheaves_obj_obj_isAddCommGroup, instFullFintypeCatLightProfiniteToLightProfinite, Condensed.instAB4CondensedMod, Condensed.equalizerCondition_profinite, Condensed.equalizerCondition, LocallyConstant.functorToPresheaves_obj_map, Profinite.isIso_asLimitCone_lift, instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite, Condensed.lanPresheafIso_hom, Condensed.discrete_obj, Stonean.effectiveEpi_tfae, coe_comp, finiteCoproduct.ι_jointly_surjective, instHasFiniteCoproductsOfHasExplicitFiniteCoproducts, LightCondensed.instPreservesFiniteProductsOppositeLightProfiniteVal, Profinite.exists_hom, LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology, pullback.cone_pt, LocallyConstant.functorToPresheaves_obj_obj, CompHausToLocale.faithful, topToCompHaus_obj, finiteCoproduct.ι_desc_apply
compHausLikeToTop 📖	CompOp	18 math math: instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts, instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions, TopCat.toSheafCompHausLike_val_obj, LightCondSet.topCatAdjunctionUnit_val_app_apply, topCatToSheafCompHausLike_map_val_app, instFullTopCatCompHausLikeToTop, instFaithfulTopCatCompHausLikeToTop, CondensedSet.topCatAdjunctionUnit_val_app_apply, instT2SpaceCarrierObjTopCatCompHausLikeToTop, instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop, CondensedSet.topCatAdjunctionUnit_val_app, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, compHausLikeToTop_map, TopCat.toSheafCompHausLike_val_map, isoOfHomeo_inv_hom_hom_apply, LightCondSet.topCatAdjunctionUnit_val_app, instCompactSpaceCarrierObjTopCatCompHausLikeToTop, isoOfHomeo_hom_hom_hom_apply
concreteCategory 📖	CompOp	43 math math: ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Profinite.forget_preservesLimits, coe_id, Profinite.effectiveEpi_tfae, LightProfinite.proj_comp_transitionMapLE', ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Profinite.epi_iff_surjective, LightProfinite.isClosedMap, isClosedMap, LightProfinite.effectiveEpi_iff_surjective, finiteCoproduct.isOpenEmbedding_ι, Sigma.isOpenEmbedding_ι, Stonean.epi_iff_surjective, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, LightCondensed.isoFinYonedaComponents_inv_comp, Profinite.exists_isClopen_of_cofiltered, Stonean.forget.preservesLimits, LightProfinite.surjective_transitionMapLE, mono_iff_injective, LightProfinite.forget_reflectsIsomorphisms, forget_reflectsIsomorphisms, Condensed.isoFinYonedaComponents_inv_comp, const_comp, finiteCoproduct.ι_injective, CompHaus.effectiveEpi_tfae, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, toCompHausLike_map, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, LightProfinite.surjective_transitionMap, CompHaus.epi_iff_surjective, LightProfinite.epi_iff_surjective, hom_ofHom, LocallyConstant.incl_comap, LightProfinite.proj_surjective, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, LightProfinite.proj_comp_transitionMap', ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, Stonean.effectiveEpi_tfae, coe_comp, finiteCoproduct.ι_jointly_surjective, finiteCoproduct.ι_desc_apply
const 📖	CompOp	7 math math: LightCondensed.isoFinYonedaComponents_hom_apply, LightCondSet.topCatAdjunctionUnit_val_app_apply, Condensed.isoFinYonedaComponents_hom_apply, CondensedSet.topCatAdjunctionUnit_val_app_apply, CondensedSet.topCatAdjunctionUnit_val_app, const_comp, LightCondSet.topCatAdjunctionUnit_val_app
fullyFaithfulCompHausLikeToTop 📖	CompOp	—
fullyFaithfulToCompHausLike 📖	CompOp	—
hasForget₂ 📖	CompOp	—
homeoOfIso 📖	CompOp	3 math math: homeoOfIso_symm_apply, homeoOfIso_apply, isoEquivHomeo_apply
instCoeSortType 📖	CompOp	—
isoEquivHomeo 📖	CompOp	2 math math: isoEquivHomeo_symm_apply, isoEquivHomeo_apply
isoOfBijective 📖	CompOp	1 math math: Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app
isoOfHomeo 📖	CompOp	3 math math: isoEquivHomeo_symm_apply, isoOfHomeo_inv_hom_hom_apply, isoOfHomeo_hom_hom_hom_apply
of 📖	CompOp	19 math math: coe_of, LocallyConstant.adjunction_counit, LocallyConstant.counitApp_app, LocallyConstant.incl_of_counitAppApp, sigmaComparison_eq_comp_isos, FintypeCat.toProfinite_map_hom_hom_apply, ofHom_id, ofHom_comp, FintypeCat.toLightProfinite_map_hom_hom_apply, LocallyConstant.adjunction_left_triangle, toCompHausLike_map, LocallyConstant.instIsIsoFunctorTypeUnitSheafCoherentTopologyAdjunction, isIsoSigmaComparison, LocallyConstant.counit_app_val, hom_ofHom, LocallyConstant.sigmaComparison_comp_sigmaIso, LocallyConstant.unit_app, LocallyConstant.incl_comap, LocallyConstant.adjunction_unit
ofHom 📖	CompOp	3 math math: ofHom_id, ofHom_comp, hom_ofHom
toCompHausLike 📖	CompOp	5 math math: instPreservesFiniteCoproductsToCompHausLike, toCompHausLike_map, instFullToCompHausLike, instPreservesLimitWalkingCospanCospanToCompHausLike, instFaithfulToCompHausLike
toTop 📖	CompOp	167 math math: ProfiniteGrp.coe_of, ProfiniteGrp.instReflectsIsomorphismsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Stonean.instExtremallyDisconnectedCarrierToTop, Profinite.forget_preservesLimits, ProfiniteGrp.limit_one_val, ProfiniteAddGrp.ofHom_hom, coe_of, ProfiniteGrp.ProfiniteCompletion.lift_eta, LightCondSet.continuous_coinducingCoprod, LightProfinite.instCountableClopensCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, CompHaus.toStonean_toTop, coe_id, LocallyConstantModule.functorToPresheaves_obj_obj_isModule, ProfiniteAddGrp.ofHom_apply, ProfiniteGrp.coe_id, Profinite.effectiveEpi_tfae, LocallyConstant.freeOfProfinite, LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, ProfiniteGrp.ProfiniteCompletion.lift_eta_assoc, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, LightProfinite.proj_comp_transitionMapLE', ProfiniteGrp.instFaithfulProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteAddGrp.instPreservesLimitsProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, Profinite.epi_iff_surjective, lightProfiniteToLightDiagram_map, Profinite.exists_locallyConstant_finite_aux, Profinite.instTotallyDisconnectedSpaceCarrierToTop, ProfiniteGrp.toLimit_surjective, LightProfinite.isClosedMap, ProfiniteAddGrp.hom_neg_apply, lightDiagramToLightProfinite_obj, ProfiniteGrp.hom_id, LocallyConstantModule.functorToPresheaves_map_app, ProfiniteAddGrp.hom_id, ProfiniteAddGrp.neg_hom_apply, homeoOfIso_symm_apply, LightProfinite.lightToProfinite_map_proj_eq, isClosedMap, FintypeCat.toProfinite_map_hom_hom_apply, ProfiniteGrp.denseRange_toLimit, ProfiniteAddGrp.limit_zero_val, ProfiniteGrp.comp_apply, isoEquivHomeo_symm_apply, LightProfinite.effectiveEpi_iff_surjective, Stonean.effectiveEpiFamily_tfae, ProfiniteAddGrp.coe_of, ProfiniteAddGrp.comp_apply, LightProfinite.continuous_iff_convergent, LightProfinite.instCountableDiscreteQuotient, ProfiniteGrp.ofHom_hom, Condensed.instPreservesLimitsOfShapeOppositeProfiniteDiscreteCarrierToTopTotallyDisconnectedSpaceOfFinite, finiteCoproduct.isOpenEmbedding_ι, Sigma.isOpenEmbedding_ι, ProfiniteGrp.topologicalGroup, ProfiniteGrp.hom_comp, InfiniteGalois.mulEquivToLimit_symm_continuous, Stonean.epi_iff_surjective, ProfiniteAddGrp.instIsTopologicalAddGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousAddMonoidHomToProfiniteContinuousMap, ProfiniteGrp.inv_hom_apply, ProfiniteAddGrp.id_apply, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, ProfiniteGrp.cone_pt, LightCondensed.isoFinYonedaComponents_inv_comp, ProfiniteAddGrp.coe_id, Condensed.isColimitLocallyConstantPresheaf_desc_apply, LocallyConstant.functorToPresheaves_map_app, Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone, InfiniteGalois.proj_adjoin_singleton_val, ProfiniteGrp.limit_mul_val, ProfiniteGrp.ProfiniteCompletion.denseRange, FintypeCat.toLightProfinite_map_hom_hom_apply, instTotallyDisconnectedSpaceCarrierToTopTrueObjProfiniteCompHausProfiniteToCompHaus, Stonean.forget.preservesLimits, instHasPropCarrierToTop, CompHaus.toProfinite_obj', Condensed.isoLocallyConstantOfIsColimit_inv, ProfiniteAddGrp.limit_add_val, LightProfinite.surjective_transitionMapLE, mono_iff_injective, LocallyConstantModule.functorToPresheaves_obj_map, ProfiniteGrp.profiniteCompletion_map, LightProfinite.forget_reflectsIsomorphisms, forget_reflectsIsomorphisms, Condensed.isoFinYonedaComponents_inv_comp, stoneCechObj_toTop_carrier, Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp, CondensedSet.continuous_coinducingCoprod, ProfiniteAddGrp.limit_ext_iff, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology, is_compact, ProfiniteGrp.hom_inv_apply, LocallyConstantModule.functorToPresheaves_obj_obj_carrier, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, ProfiniteGrp.cone_π_app, const_comp, finiteCoproduct.ι_injective, LightProfinite.instTotallyDisconnectedSpaceCarrierToTopTruePtCompHausLimitConeCompLightProfiniteToCompHaus, Profinite.exists_locallyConstant, CompHaus.effectiveEpi_tfae, LightProfinite.instPreservesLimitsOfShapeOppositeNatForgetContinuousMapCarrierToTopAndTotallyDisconnectedSpaceSecondCountableTopology, InfiniteGalois.toAlgEquivAux_eq_liftNormal, homeoOfIso_apply, ProfiniteGrp.toLimit_injective, ProfiniteAddGrp.coe_comp, LightDiagram.id_hom_hom_hom_apply, ProfiniteGrp.ofHom_apply, compHausLikeToTop_map, ProfiniteGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemSubgroupLimitConePtAux, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, LightCondSet.LocallyConstant.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopologySubtypeToTop, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, CompHaus.instCompactSpaceCarrierToTopTrue, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, lightDiagramToLightProfinite_map, LightProfinite.surjective_transitionMap, CompHaus.epi_iff_surjective, ProfiniteGrp.coe_comp, LightProfinite.epi_iff_surjective, InfiniteGalois.mk_toAlgEquivAux, isoOfHomeo_inv_hom_hom_apply, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CompHaus.Gleason, hom_ofHom, prop, InfiniteGalois.proj_of_le, LightDiagram.comp_hom_hom_hom_apply, ProfiniteGrp.toLimitFun_continuous, ProfiniteGrp.diagram_map, InfiniteGalois.algEquivToLimit_continuous, ProfiniteGrp.id_apply, Profinite.Nobeling.isClosedEmbedding, LightProfinite.proj_surjective, isoEquivHomeo_apply, ProfiniteGrp.isIso_toLimit, is_hausdorff, instSecondCountableTopologyCarrierToTopTotallyDisconnectedSpacePtOppositeNatProfiniteCone, InfiniteGalois.limitToAlgEquiv_symm_apply, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, isoOfHomeo_hom_hom_hom_apply, CompHaus.effectiveEpiFamily_tfae, Profinite.exists_locallyConstant_finite_nonempty, ProfiniteGrp.instPreservesLimitsProfiniteForget₂ContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap, ProfiniteGrp.limit_ext_iff, CompHaus.instExtremallyDisconnectedCarrierToTopTrueOfProjective, Profinite.exists_locallyConstant_fin_two, ProfiniteAddGrp.hom_comp, Profinite.effectiveEpiFamily_tfae, LightProfinite.proj_comp_transitionMap', ProfiniteGrp.instIsTopologicalGroupCarrierToTopTotallyDisconnectedSpacePtProfiniteLimitConeCompForget₂ContinuousMonoidHomToProfiniteContinuousMap, Condensed.locallyConstantIsoFinYoneda_hom_app, ProfiniteAddGrp.instCompactSpaceSubtypeForallCarrierToTopTotallyDisconnectedSpaceToProfiniteObjMemAddSubgroupLimitConePtAux, LocallyConstantModule.functorToPresheaves_obj_obj_isAddCommGroup, LocallyConstant.functorToPresheaves_obj_map, Profinite.isIso_asLimitCone_lift, Stonean.effectiveEpi_tfae, coe_comp, finiteCoproduct.ι_jointly_surjective, ProfiniteAddGrp.topologicalAddGroup, LocallyConstant.functorToPresheaves_obj_obj, ProfiniteGrp.diagram_obj, topToCompHaus_obj, finiteCoproduct.ι_desc_apply, ProfiniteGrp.instReflectsIsomorphismsForgetContinuousMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfinite, CompHaus.instT2SpaceCarrierToTopTrue

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_comp 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	—	—
coe_id 📖	mathematical	—	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_of 📖	mathematical	—	TopCat.carrier toTop of	—	—
compHausLikeToTop_map 📖	mathematical	—	CategoryTheory.Functor.map CompHausLike category TopCat TopCat.instCategory compHausLikeToTop CategoryTheory.InducedCategory.Hom.hom toTop	—	—
const_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CompHausLike CategoryTheory.Category.toCategoryStruct category const DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory	—	—
epi_of_surjective 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory	CategoryTheory.Epi	—	CategoryTheory.Functor.epi_of_epi_map CategoryTheory.Functor.reflectsEpimorphisms_of_faithful CategoryTheory.instFaithfulForget CategoryTheory.epi_iff_surjective
forget_reflectsIsomorphisms 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms CompHausLike category CategoryTheory.types CategoryTheory.forget ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory	—	isIso_of_bijective CategoryTheory.isIso_iff_bijective
hom_ofHom 📖	mathematical	—	CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory of ofHom	—	—
homeoOfIso_apply 📖	mathematical	—	DFunLike.coe Homeomorph TopCat.carrier toTop TopCat.str EquivLike.toFunLike Homeomorph.instEquivLike homeoOfIso ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.InducedCategory.Hom.hom CompHausLike CategoryTheory.Iso.hom category	—	—
homeoOfIso_symm_apply 📖	mathematical	—	DFunLike.coe Homeomorph TopCat.carrier toTop TopCat.str EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm homeoOfIso ContinuousMap ContinuousMap.instFunLike CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory TopCat.instConcreteCategoryContinuousMapCarrier CategoryTheory.InducedCategory.Hom.hom CompHausLike CategoryTheory.Iso.inv category	—	—
instCompactSpaceCarrierObjTopCatCompHausLikeToTop 📖	mathematical	—	CompactSpace TopCat.carrier CategoryTheory.Functor.obj CompHausLike category TopCat TopCat.instCategory compHausLikeToTop TopCat.str	—	is_compact
instFaithfulToCompHausLike 📖	mathematical	toTop	CategoryTheory.Functor.Faithful CompHausLike category toCompHausLike	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulTopCatCompHausLikeToTop 📖	mathematical	—	CategoryTheory.Functor.Faithful CompHausLike category TopCat TopCat.instCategory compHausLikeToTop	—	CategoryTheory.InducedCategory.faithful
instFullToCompHausLike 📖	mathematical	toTop	CategoryTheory.Functor.Full CompHausLike category toCompHausLike	—	CategoryTheory.Functor.FullyFaithful.full
instFullTopCatCompHausLikeToTop 📖	mathematical	—	CategoryTheory.Functor.Full CompHausLike category TopCat TopCat.instCategory compHausLikeToTop	—	CategoryTheory.InducedCategory.full
instHasPropCarrierToTop 📖	mathematical	—	HasProp TopCat.carrier toTop TopCat.str	—	prop
instT2SpaceCarrierObjTopCatCompHausLikeToTop 📖	mathematical	—	T2Space TopCat.carrier CategoryTheory.Functor.obj CompHausLike category TopCat TopCat.instCategory compHausLikeToTop TopCat.str	—	is_hausdorff
isClosedMap 📖	mathematical	—	IsClosedMap TopCat.str toTop DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier ContinuousMap.instFunLike concreteCategory	—	IsCompact.isClosed is_hausdorff IsCompact.image IsClosed.isCompact is_compact ContinuousMap.continuous
isIso_of_bijective 📖	mathematical	Function.Bijective DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory	CategoryTheory.IsIso	—	continuous_iff_isClosed Equiv.image_eq_preimage_symm isClosedMap is_compact is_hausdorff instHasPropCarrierToTop CategoryTheory.ConcreteCategory.ext ContinuousMap.ext Equiv.symm_apply_apply Equiv.apply_symm_apply
is_compact 📖	mathematical	—	CompactSpace TopCat.carrier toTop TopCat.str	—	—
is_hausdorff 📖	mathematical	—	T2Space TopCat.carrier toTop TopCat.str	—	—
isoEquivHomeo_apply 📖	mathematical	—	DFunLike.coe Equiv CategoryTheory.Iso CompHausLike category Homeomorph TopCat.carrier toTop TopCat.str EquivLike.toFunLike Equiv.instEquivLike isoEquivHomeo homeoOfIso	—	—
isoEquivHomeo_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Homeomorph TopCat.carrier toTop TopCat.str CategoryTheory.Iso CompHausLike category EquivLike.toFunLike Equiv.instEquivLike Equiv.symm isoEquivHomeo isoOfHomeo	—	—
isoOfHomeo_hom_hom_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap TopCat.carrier CategoryTheory.Functor.obj CompHausLike category TopCat TopCat.instCategory compHausLikeToTop TopCat.str ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom toTop CategoryTheory.Iso.hom isoOfHomeo Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike	—	—
isoOfHomeo_inv_hom_hom_apply 📖	mathematical	—	DFunLike.coe ContinuousMap TopCat.carrier CategoryTheory.Functor.obj CompHausLike category TopCat TopCat.instCategory compHausLikeToTop TopCat.str ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom toTop CategoryTheory.Iso.inv isoOfHomeo Homeomorph EquivLike.toFunLike Homeomorph.instEquivLike Homeomorph.symm	—	—
mono_iff_injective 📖	mathematical	—	CategoryTheory.Mono CompHausLike category DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory	—	is_compact is_hausdorff instHasPropCarrierToTop continuous_const CategoryTheory.ConcreteCategory.ext ContinuousMap.ext CategoryTheory.congr_fun CategoryTheory.cancel_mono CategoryTheory.mono_iff_injective CategoryTheory.Functor.mono_of_mono_map CategoryTheory.Functor.reflectsMonomorphisms_of_faithful CategoryTheory.instFaithfulForget
ofHom_comp 📖	mathematical	—	ofHom ContinuousMap.comp CategoryTheory.CategoryStruct.comp CompHausLike CategoryTheory.Category.toCategoryStruct category of	—	—
ofHom_id 📖	mathematical	—	ofHom ContinuousMap.id CategoryTheory.CategoryStruct.id CompHausLike CategoryTheory.Category.toCategoryStruct category of	—	—
prop 📖	mathematical	—	toTop	—	—
toCompHausLike_map 📖	mathematical	toTop	CategoryTheory.Functor.map CompHausLike category toCompHausLike CategoryTheory.ConcreteCategory.ofHom ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike concreteCategory of is_compact is_hausdorff TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom TopCat TopCat.instCategory	—	is_compact is_hausdorff

CompHausLike.HasProp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasProp 📖	mathematical	—	TopCat.of	—	—

(root)

Definitions

Name	Category	Theorems
CompHausLike 📖	CompData	87 math math: CompHausLike.instPreservesFiniteCoproductsTopCatCompHausLikeToTopOfHasExplicitFiniteCoproducts, LightCondensed.isoFinYonedaComponents_hom_apply, CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions, CompHausLike.instPreservesPullbacksOfInclusionsTopCatCompHausLikeToTopOfHasExplicitPullbacksOfInclusions, CompHausLike.pullback.condition, CompHausLike.coe_id, CompHausLike.finiteCoproduct.ι_desc, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isModule, CompHausLike.HasExplicitPullbacksOfInclusions.hasProp, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe, CompHausLike.pullback.isLimit_lift, LightCondSet.topCatAdjunctionUnit_val_app_apply, lightProfiniteToLightDiagram_map, Profinite.exists_locallyConstant_finite_aux, CompHausLike.LocallyConstant.counitApp_app, Condensed.isoFinYonedaComponents_hom_apply, CompHausLike.LocallyConstantModule.functorToPresheaves_map_app, CompHausLike.homeoOfIso_symm_apply, CompHausLike.instFullTopCatCompHausLikeToTop, CompHausLike.LocallyConstant.incl_of_counitAppApp, CompHausLike.isClosedMap, CompHausLike.sigmaComparison_eq_comp_isos, FintypeCat.toProfinite_map_hom_hom_apply, CompHausLike.isoEquivHomeo_symm_apply, CompHausLike.finiteCoproduct.isOpenEmbedding_ι, CompHausLike.Sigma.isOpenEmbedding_ι, CompHausLike.instFaithfulTopCatCompHausLikeToTop, LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CompHausLike.instHasPullbacksOfInclusionsOfHasExplicitPullbacksOfInclusions, Condensed.isColimitLocallyConstantPresheaf_desc_apply, CompHausLike.LocallyConstant.functorToPresheaves_map_app, CondensedSet.topCatAdjunctionUnit_val_app_apply, CompHausLike.ofHom_id, CompHausLike.instT2SpaceCarrierObjTopCatCompHausLikeToTop, CompHausLike.ofHom_comp, FintypeCat.toLightProfinite_map_hom_hom_apply, CompHausLike.instHasPullbacksOfHasExplicitPullbacks, CompHausLike.instHasCoproduct, CompHausLike.mono_iff_injective, CompHausLike.finiteCoproduct.ι_desc_assoc, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_map, CompHausLike.forget_reflectsIsomorphisms, CompHausLike.instPreservesLimitTopCatWalkingCospanCospanCompHausLikeToTop, CondensedSet.topCatAdjunctionUnit_val_app, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_carrier, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_hom_app_val_app_apply, CompHausLike.pullback.condition_assoc, CompHausLike.pullback.cone_π, CompHausLike.const_comp, CompHausLike.finiteCoproduct.ι_injective, Profinite.exists_locallyConstant, CompHausLike.homeoOfIso_apply, LightDiagram.id_hom_hom_hom_apply, CompHausLike.instHasLimitWalkingCospanCospan, CompHausLike.compHausLikeToTop_map, CompHausLike.instPreservesFiniteCoproductsToCompHausLike, CompHausLike.toCompHausLike_map, Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply, CompHausLike.isIsoSigmaComparison, Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app, lightDiagramToLightProfinite_map, CompHausLike.isoOfHomeo_inv_hom_hom_apply, LightCondensed.isColimitLocallyConstantPresheaf_desc_apply, CompHausLike.hom_ofHom, CompHausLike.instFullToCompHausLike, CompHausLike.LocallyConstant.sigmaComparison_comp_sigmaIso, CompHausLike.instPreservesLimitWalkingCospanCospanToCompHausLike, LightCondSet.topCatAdjunctionUnit_val_app, LightDiagram.comp_hom_hom_hom_apply, CompHausLike.LocallyConstant.incl_comap, CompHausLike.isoEquivHomeo_apply, CompHausLike.finitaryExtensive, lightProfiniteToLightCondSetIsoTopCatToLightCondSet_inv_app_val_app_hom_hom, CompHausLike.instCompactSpaceCarrierObjTopCatCompHausLikeToTop, CompHausLike.isoOfHomeo_hom_hom_hom_apply, CompHausLike.instFaithfulToCompHausLike, Profinite.exists_locallyConstant_finite_nonempty, Profinite.exists_locallyConstant_fin_two, CompHausLike.LocallyConstantModule.functorToPresheaves_obj_obj_isAddCommGroup, CompHausLike.LocallyConstant.functorToPresheaves_obj_map, CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite, CompHausLike.coe_comp, CompHausLike.finiteCoproduct.ι_jointly_surjective, CompHausLike.instHasFiniteCoproductsOfHasExplicitFiniteCoproducts, CompHausLike.pullback.cone_pt, CompHausLike.LocallyConstant.functorToPresheaves_obj_obj, CompHausLike.finiteCoproduct.ι_desc_apply

---

← Back to Index