Documentation Verification Report

EffectiveEpi

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

Statistics

Metric	Count
Definitions `stoneanToCompHausEffectivePresentation`	1
Theorems `effectiveEpiFamily_of_jointly_surjective`, `effectiveEpiFamily_tfae`, `effectiveEpi_tfae`, `instEffectivelyEnoughCompHausToCompHaus`, `instPreregular`, `instPreservesEffectiveEpisCompHausToCompHaus`, `instReflectsEffectiveEpisCompHausToCompHaus`	7
Total	8

Stonean

Definitions

Name	Category	Theorems
`stoneanToCompHausEffectivePresentation` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`effectiveEpiFamily_of_jointly_surjective` 📖	mathematical	`DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `ContinuousMap` `CompHausLike.toTop` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	`CategoryTheory.EffectiveEpiFamily`	—	`List.TFAE.out` `CompHausLike.instHasCoproduct` `instHasPropExtremallyDisconnectedCarrier` `instExtremallyDisconnected` `instExtremallyDisconnectedCarrierToTop` `effectiveEpiFamily_tfae`
`effectiveEpiFamily_tfae` 📖	mathematical	—	`List.TFAE` `CategoryTheory.EffectiveEpiFamily` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `CategoryTheory.Epi` `CategoryTheory.Limits.sigmaObj` `CompHausLike.instHasCoproduct` `instHasPropExtremallyDisconnectedCarrier` `CompHausLike.toTop` `instTopologicalSpaceSigma` `instExtremallyDisconnected` `instExtremallyDisconnectedCarrierToTop` `CategoryTheory.Limits.Sigma.desc`	—	`CompHausLike.instHasCoproduct` `instHasPropExtremallyDisconnectedCarrier` `instExtremallyDisconnected` `instExtremallyDisconnectedCarrierToTop` `CategoryTheory.Limits.hasColimitOfHasColimitsOfShape` `CategoryTheory.Limits.hasColimitsOfShape_discrete` `CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts` `CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive` `CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions` `instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier` `instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier` `List.TFAE.out` `effectiveEpi_tfae` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiDescOfEffectiveEpiFamily` `CompHaus.instHasPropTrue` `CompHaus.effectiveEpiFamily_tfae` `CategoryTheory.Functor.finite_effectiveEpiFamily_of_map` `CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis` `CompHaus.instHasExplicitFiniteCoproductsTrue` `CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks` `CompHaus.instHasExplicitPullbacksTrue` `CompHausLike.instPreservesFiniteCoproductsToCompHausLike` `instReflectsEffectiveEpisCompHausToCompHaus` `CategoryTheory.Functor.map_finite_effectiveEpiFamily` `CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis` `instPreservesEffectiveEpisCompHausToCompHaus` `List.tfae_of_cycle`
`effectiveEpi_tfae` 📖	mathematical	—	`List.TFAE` `CategoryTheory.EffectiveEpi` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `CategoryTheory.Epi` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `CompHausLike.toTop` `ContinuousMap.instFunLike` `CompHausLike.concreteCategory`	—	`CategoryTheory.epi_of_effectiveEpi` `epi_iff_surjective` `List.tfae_of_cycle`
`instEffectivelyEnoughCompHausToCompHaus` 📖	mathematical	—	`CategoryTheory.Functor.EffectivelyEnough` `Stonean` `CompHaus` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `toCompHaus`	—	—
`instPreregular` 📖	mathematical	—	`CategoryTheory.Preregular` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str`	—	`CategoryTheory.Functor.reflects_preregular` `instPreservesEffectiveEpisCompHausToCompHaus` `instReflectsEffectiveEpisCompHausToCompHaus` `instEffectivelyEnoughCompHausToCompHaus` `CompHaus.instPreregular` `CompHausLike.instFullToCompHausLike` `CompHausLike.instFaithfulToCompHausLike`
`instPreservesEffectiveEpisCompHausToCompHaus` 📖	mathematical	—	`CategoryTheory.Functor.PreservesEffectiveEpis` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `CompHaus` `toCompHaus`	—	`List.TFAE.out` `CompHaus.effectiveEpi_tfae` `effectiveEpi_tfae`
`instReflectsEffectiveEpisCompHausToCompHaus` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsEffectiveEpis` `Stonean` `CompHausLike.category` `ExtremallyDisconnected` `TopCat.carrier` `TopCat.str` `CompHaus` `toCompHaus`	—	`List.TFAE.out` `effectiveEpi_tfae` `CompHaus.effectiveEpi_tfae`

---

← Back to Index