EffectiveEpi

Statistics

Metric	Count
Definitions	0
Theorems `effectiveEpi_iff_surjective`, `instPreregular`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpi_iff_surjective` 📖	mathematical	—	`CategoryTheory.EffectiveEpi` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `CompHausLike.toTop` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	—	`epi_iff_surjective` `CategoryTheory.epi_of_effectiveEpi`
`instPreregular` 📖	mathematical	—	`CategoryTheory.Preregular` `LightProfinite` `CompHausLike.category` `TotallyDisconnectedSpace` `TopCat.carrier` `TopCat.str` `SecondCountableTopology`	—	`CompHausLike.preregular` `instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology` `effectiveEpi_iff_surjective`

---