Over

Statistics

Metric	Count
Definitions	0
Theorems `instPreservesCofilteredLimitsOfSizeOverForget`, `instPreservesFilteredColimitsOfSizeUnderForget`	2
Total	2

Name	Kind	Assumes	Proves	Validates	Depends On
`instPreservesCofilteredLimitsOfSizeOverForget` 📖	mathematical	—	`PreservesCofilteredLimitsOfSize` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `CategoryTheory.Over.forget`	—	`CategoryTheory.IsCofiltered.nonempty` `CategoryTheory.IsCofilteredOrEmpty.cone_objs` `CategoryTheory.IsCofiltered.toIsCofilteredOrEmpty` `Cone.w` `CategoryTheory.Category.assoc` `CategoryTheory.Over.w` `CategoryTheory.Over.OverMorphism.ext` `CategoryTheory.Category.id_comp` `IsLimit.fac` `IsLimit.uniq`
`instPreservesFilteredColimitsOfSizeUnderForget` 📖	mathematical	—	`PreservesFilteredColimitsOfSize` `CategoryTheory.Under` `CategoryTheory.instCategoryUnder` `CategoryTheory.Under.forget`	—	`CategoryTheory.IsFiltered.nonempty` `CategoryTheory.IsFilteredOrEmpty.cocone_objs` `CategoryTheory.IsFiltered.toIsFilteredOrEmpty` `Cocone.w` `CategoryTheory.Under.w_assoc` `CategoryTheory.Under.UnderMorphism.ext` `CategoryTheory.Category.comp_id` `IsColimit.fac` `IsColimit.uniq`

---