Enough

📁 Source: Mathlib/CategoryTheory/EffectiveEpi/Enough.lean

Statistics

Metric	Count
Definitions EffectivePresentation, f, p, EffectivelyEnough, effectiveEpiOver, effectiveEpiOverObj, equivalenceEffectivePresentation	7
Theorems effectiveEpi, presentation, instEffectiveEpiEffectiveEpiOver, instEffectivelyEnoughOfIsEquivalence	4
Total	11

CategoryTheory.Functor

Definitions

Name	Category	Theorems
EffectivePresentation 📖	CompData	1 math math: EffectivelyEnough.presentation
EffectivelyEnough 📖	CompData	4 math math: Stonean.instEffectivelyEnoughCompHausToCompHaus, instEffectivelyEnoughOfIsEquivalence, Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite, Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus
effectiveEpiOver 📖	CompOp	1 math math: instEffectiveEpiEffectiveEpiOver
effectiveEpiOverObj 📖	CompOp	1 math math: instEffectiveEpiEffectiveEpiOver
equivalenceEffectivePresentation 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEffectiveEpiEffectiveEpiOver 📖	mathematical	—	CategoryTheory.EffectiveEpi effectiveEpiOverObj effectiveEpiOver	—	EffectivePresentation.effectiveEpi EffectivelyEnough.presentation
instEffectivelyEnoughOfIsEquivalence 📖	mathematical	—	EffectivelyEnough	—	—

CategoryTheory.Functor.EffectivePresentation

Definitions

Name	Category	Theorems
f 📖	CompOp	1 math math: effectiveEpi
p 📖	CompOp	1 math math: effectiveEpi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
effectiveEpi 📖	mathematical	—	CategoryTheory.EffectiveEpi CategoryTheory.Functor.obj p f	—	—

CategoryTheory.Functor.EffectivelyEnough

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
presentation 📖	mathematical	—	CategoryTheory.Functor.EffectivePresentation	—	—

---

← Back to Index