LocallySmall

Statistics

Name	Category	Theorems
`LocallySmall` 📖	CompData	33 math math: `IsGrothendieckAbelian.locallySmall`, `locallySmall_fullSubcategory`, `HomotopicalAlgebra.BifibrantObject.instLocallySmallHoCat`, `instLocallySmallFunctor`, `locallySmall_max`, `locallySmall_of_thin`, `Shrink.instLocallySmallShrink`, `instLocallySmallSmallModel`, `essentiallySmall_iff`, `Over.locallySmall`, `Limits.ColimitPresentation.instLocallySmallTotal`, `locallySmall_of_essentiallySmall`, `instLocallySmallFullSubcategoryFunctorOppositeTypeIsIndObject`, `CountableCategory.instLocallySmallObjAsType`, `CategoryOfElements.instLocallySmallElements`, `Limits.WalkingMultispan.instLocallySmall`, `Quotient.instLocallySmall`, `locallySmall_of_univLE`, `locallySmall_of_faithful`, `SmallObject.locallySmall`, `locallySmall_congr`, `Under.locallySmall`, `instLocallySmallOpposite`, `Comma.locallySmall`, `HomotopicalAlgebra.locallySmall_of_isLocalization`, `StructuredArrow.locallySmall`, `HomologicalComplex.locallySmall`, `locallySmall_of_small_arrow`, `MorphismProperty.IsCardinalForSmallObjectArgument.locallySmall`, `HasCardinalFilteredGenerator.toLocallySmall`, `MorphismProperty.locallySmall_of_hasLocalization`, `CostructuredArrow.locallySmall`, `locallySmall_self`

Name	Kind	Assumes	Proves	Validates	Depends On
`instLocallySmall` 📖	mathematical	—	`CategoryTheory.LocallySmall` `CategoryTheory.Quotient` `category`	—	`small_of_surjective` `CategoryTheory.instSmallHomOfLocallySmall` `CategoryTheory.Functor.map_surjective` `full_functor`

---