EffectiveEpi

Statistics

Metric	Count
Definitions	0
Theorems `instIsRegularEpiCategoryCondensedSet`, `instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsRegularEpiCategoryCondensedSet` 📖	mathematical	—	`CategoryTheory.IsRegularEpiCategory` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types`	—	`CategoryTheory.instIsRegularEpiCategorySheafTypeOfHasSheafify` `CategoryTheory.instHasSheafifyType`
`instPreservesEpimorphismsCompHausCondensedSetCompHausToCondensed` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEpimorphisms` `CompHaus` `CompHausLike.category` `CondensedSet` `instCategoryCondensed` `CategoryTheory.types` `compHausToCondensed`	—	`CondensedSet.epi_iff_locallySurjective_on_compHaus` `CompHaus.instHasPropTrue` `CompHaus.epi_iff_surjective` `ULift.ext` `CompHausLike.pullback.condition`

---