Small

📁 Source: Mathlib/Condensed/Light/Small.lean

Statistics

Metric	Count
Definitions equivSmall, equivSmallFreeIso, equivSmallSheafificationIso	3
Theorems instSmallHom	1
Total	4

LightCondensed

Definitions

Name	Category	Theorems
equivSmall 📖	CompOp	—
equivSmallFreeIso 📖	CompOp	—
equivSmallSheafificationIso 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instSmallHom 📖	mathematical	—	Small Quiver.Hom LightCondensed CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategoryLightCondensed	—	instEssentiallySmallLightProfinite CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse

---

← Back to Index