EffectiveEpi

📁 Source: Mathlib/Topology/Category/CompHaus/EffectiveEpi.lean

Statistics

Metric	Count
Definitions	0
Theorems effectiveEpiFamily_of_jointly_surjective, effectiveEpiFamily_tfae, effectiveEpi_tfae, instPreregular	4
Total	4

CompHaus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpiFamily_of_jointly_surjective 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHaus CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.EffectiveEpiFamily	—	List.TFAE.out CompHausLike.instHasCoproduct instHasPropTrue effectiveEpiFamily_tfae
effectiveEpiFamily_tfae 📖	mathematical	—	List.TFAE CategoryTheory.EffectiveEpiFamily CompHaus CompHausLike.category CategoryTheory.Epi CategoryTheory.Limits.sigmaObj CompHausLike.instHasCoproduct instHasPropTrue TopCat.carrier CompHausLike.toTop instTopologicalSpaceSigma TopCat.str CategoryTheory.Limits.Sigma.desc	—	CompHausLike.instHasCoproduct instHasPropTrue CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks instHasExplicitPullbacksTrue List.TFAE.out effectiveEpi_tfae CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiDescOfEffectiveEpiFamily epi_iff_surjective CategoryTheory.Limits.colimit.ι_desc CategoryTheory.Iso.hom_inv_id CategoryTheory.Iso.inv_comp_eq CategoryTheory.Limits.colimit.hom_ext CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom_assoc CategoryTheory.ConcreteCategory.ext ContinuousMap.ext List.tfae_of_cycle
effectiveEpi_tfae 📖	mathematical	—	List.TFAE CategoryTheory.EffectiveEpi CompHaus CompHausLike.category CategoryTheory.Epi DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	—	CategoryTheory.epi_of_effectiveEpi epi_iff_surjective List.tfae_of_cycle
instPreregular 📖	mathematical	—	CategoryTheory.Preregular CompHaus CompHausLike.category	—	CompHausLike.preregular instHasExplicitPullbacksTrue List.TFAE.out effectiveEpi_tfae

---

← Back to Index