Small

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Small.lean

Statistics

Metric	Count
Definitions Small	1
Theorems exists_small, exists_small_le, exists_small_le', of_le, of_le, essentiallySmall_op_iff, essentiallySmall_unop_iff, exists_equivalence_iff, instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall, instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1, instEssentiallySmallISupOfSmall, instEssentiallySmallIsoClosure, instEssentiallySmallMap, instEssentiallySmallMax, instEssentiallySmallOfSmall, instEssentiallySmallOppositeOp, instEssentiallySmallTopOfEssentiallySmall, instEssentiallySmallUnopOfOpposite, instSmallFullSubcategoryOfSmall, instSmallISupOfSmall, instSmallMax, instSmallMin, instSmallMin_1, instSmallOfObjOfSmall, instSmallOppositeOp, instSmallOppositeOp_1, instSmallPair, instSmallStrictMap, instSmallUnopOfOpposite, instSmallUnopOfOpposite_1, small_op_iff, small_unop_iff, exists_equivalence_iff_of_locallySmall	33
Total	34

CategoryTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_equivalence_iff_of_locallySmall 📖	mathematical	—	Equivalence ObjectProperty.EssentiallySmall Top.top ObjectProperty Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	ObjectProperty.exists_equivalence_iff

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
Small 📖	MathDef	21 math math: instSmallUnopOfOpposite_1, CategoryTheory.CostructuredArrow.small_proj_preimage_of_locallySmall, Small.of_le, instSmallOppositeOp, CategoryTheory.StructuredArrow.small_inverseImage_proj_of_locallySmall, instSmallMin, instSmallOppositeOp_1, PresheafOfModules.freeYoneda.instSmall, instSmallOfObjOfSmall, instSmallPair, instSmallStrictColimitsOfShapeOfSmallOfLocallySmall, instSmallStrictLimitsOfShapeOfSmallOfLocallySmall, instSmallMax, instSmallMin_1, small_unop_iff, instSmallStrictLimitsClosureIterOfLocallySmallOfSmallElemIio, instSmallStrictMap, small_op_iff, CategoryTheory.CostructuredArrow.small_inverseImage_proj_of_locallySmall, instSmallUnopOfOpposite, CategoryTheory.StructuredArrow.small_proj_preimage_of_locallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essentiallySmall_op_iff 📖	mathematical	—	EssentiallySmall Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	EssentiallySmall.exists_small_le instSmallUnopOfOpposite_1 unop_isoClosure op_monotone_iff op_unop instSmallOppositeOp_1 op_isoClosure
essentiallySmall_unop_iff 📖	mathematical	—	EssentiallySmall unop CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite	—	essentiallySmall_op_iff op_unop
exists_equivalence_iff 📖	mathematical	—	CategoryTheory.Equivalence FullSubcategory FullSubcategory.category EssentiallySmall	—	instSmallOfObjOfSmall UnivLE.small UnivLE.self EssentiallySmall.exists_small_le instSmallFullSubcategoryOfSmall CategoryTheory.Shrink.instLocallySmallShrink CategoryTheory.locallySmall_fullSubcategory isEquivalence_ιOfLE_iff
instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall 📖	mathematical	—	CategoryTheory.EssentiallySmall FullSubcategory FullSubcategory.category	—	EssentiallySmall.exists_small_le isEquivalence_ιOfLE_iff CategoryTheory.essentiallySmall_congr CategoryTheory.essentiallySmall_of_small_of_locallySmall instSmallFullSubcategoryOfSmall CategoryTheory.locallySmall_fullSubcategory
instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1 📖	mathematical	—	CategoryTheory.EssentiallySmall FullSubcategory FullSubcategory.category	—	EssentiallySmall.exists_small_le isEquivalence_ιOfLE_iff CategoryTheory.essentiallySmall_congr CategoryTheory.essentiallySmall_of_small_of_locallySmall instSmallFullSubcategoryOfSmall CategoryTheory.locallySmall_fullSubcategory
instEssentiallySmallISupOfSmall 📖	mathematical	EssentiallySmall	iSup CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.supSet CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Prop.instCompleteLattice	—	EssentiallySmall.exists_small_le' instSmallISupOfSmall LE.le.trans monotone_isoClosure le_iSup
instEssentiallySmallIsoClosure 📖	mathematical	—	EssentiallySmall isoClosure	—	EssentiallySmall.exists_small_le isoClosure_le_iff instIsClosedUnderIsomorphismsIsoClosure
instEssentiallySmallMap 📖	mathematical	—	EssentiallySmall map	—	EssentiallySmall.exists_small_le instSmallStrictMap LE.le.trans map_monotone map_isoClosure isoClosure_strictMap
instEssentiallySmallMax 📖	mathematical	—	EssentiallySmall CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMaxForall_mathlib SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice Prop.instCompleteLattice	—	EssentiallySmall.exists_small_le' instSmallMax LE.le.trans monotone_isoClosure le_sup_left le_sup_right
instEssentiallySmallOfSmall 📖	mathematical	—	EssentiallySmall	—	le_isoClosure
instEssentiallySmallOppositeOp 📖	mathematical	—	EssentiallySmall Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	—
instEssentiallySmallTopOfEssentiallySmall 📖	mathematical	—	EssentiallySmall Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	instSmallOfObjOfSmall UnivLE.small UnivLE.self
instEssentiallySmallUnopOfOpposite 📖	mathematical	—	EssentiallySmall unop CategoryTheory.Category.toCategoryStruct	—	—
instSmallFullSubcategoryOfSmall 📖	mathematical	—	Small FullSubcategory	—	small_of_surjective FullSubcategory.property
instSmallISupOfSmall 📖	mathematical	Small	iSup CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.supSet CompleteSemilatticeSup.toSupSet CompleteLattice.toCompleteSemilatticeSup Prop.instCompleteLattice	—	small_of_surjective small_sigma
instSmallMax 📖	mathematical	—	Small CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMaxForall_mathlib SemilatticeSup.toMax Lattice.toSemilatticeSup CompleteLattice.toLattice Prop.instCompleteLattice	—	small_of_surjective small_sum
instSmallMin 📖	mathematical	—	Small CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice Prop.instCompleteLattice	—	Small.of_le inf_le_right
instSmallMin_1 📖	mathematical	—	Small CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf CompleteLattice.toLattice Prop.instCompleteLattice	—	Small.of_le inf_le_left
instSmallOfObjOfSmall 📖	mathematical	—	Small ofObj CategoryTheory.Category.toCategoryStruct	—	small_of_surjective
instSmallOppositeOp 📖	mathematical	—	Small Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	small_of_injective Equiv.injective
instSmallOppositeOp_1 📖	mathematical	—	Small Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	—
instSmallPair 📖	mathematical	—	Small pair CategoryTheory.Category.toCategoryStruct	—	instSmallOfObjOfSmall small_sum UnivLE.small univLE_of_max UnivLE.self
instSmallStrictMap 📖	mathematical	—	Small strictMap	—	small_of_surjective
instSmallUnopOfOpposite 📖	mathematical	—	Small unop CategoryTheory.Category.toCategoryStruct	—	small_congr
instSmallUnopOfOpposite_1 📖	mathematical	—	Small unop CategoryTheory.Category.toCategoryStruct	—	—
small_op_iff 📖	mathematical	—	Small Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	small_congr
small_unop_iff 📖	mathematical	—	Small unop CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite	—	small_op_iff op_unop

CategoryTheory.ObjectProperty.EssentiallySmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_small 📖	mathematical	—	CategoryTheory.ObjectProperty.isoClosure	—	exists_small_le le_antisymm CategoryTheory.ObjectProperty.isoClosure_le_iff
exists_small_le 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.ObjectProperty.isoClosure	—	exists_small_le' small_of_surjective CategoryTheory.ObjectProperty.instSmallMin_1
exists_small_le' 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.ObjectProperty.isoClosure	—	—
of_le 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty.EssentiallySmall	—	exists_small_le' LE.le.trans

CategoryTheory.ObjectProperty.Small

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_le 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty.Small	—	small_of_injective Subtype.map_injective

---

← Back to Index