EffectiveEpi

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

Statistics

Metric	Count
Definitions effectiveEpiStruct	1
Theorems precoherent, preregular	2
Total	3

CompHausLike

Definitions

Name	Category	Theorems
effectiveEpiStruct 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
precoherent 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory	CategoryTheory.Precoherent	—	preregular CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks
preregular 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike category ContinuousMap TopCat.carrier toTop TopCat.str ContinuousMap.instFunLike concreteCategory	CategoryTheory.Preregular	—	HasExplicitPullbacks.hasProp pullback.condition

---

← Back to Index