EffectiveEpi

Statistics

Metric	Count
Definitions	0
Theorems `instIsRegularEpiCategoryLightCondSet`, `instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsRegularEpiCategoryLightCondSet` 📖	mathematical	—	`CategoryTheory.IsRegularEpiCategory` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types`	—	`CategoryTheory.instIsRegularEpiCategorySheafTypeOfHasSheafify` `LightProfinite.hasSheafify_type`
`instPreservesEpimorphismsLightProfiniteLightCondSetLightProfiniteToLightCondSet` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `LightCondSet` `instCategoryLightCondensed` `CategoryTheory.types` `lightProfiniteToLightCondSet`	—	`LightCondSet.epi_iff_locallySurjective_on_lightProfinite` `LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `Subtype.totallyDisconnectedSpace` `Prod.totallyDisconnectedSpace` `LightProfinite.instTotallyDisconnectedSpaceCarrierToTopAndSecondCountableTopology` `TopologicalSpace.Subtype.secondCountableTopology` `TopologicalSpace.instSecondCountableTopologyProd` `LightProfinite.instSecondCountableTopologyCarrierToTopAndTotallyDisconnectedSpace` `LightProfinite.epi_iff_surjective` `CompHausLike.pullback.condition`

---