EssentiallyLarge

📁 Source: Mathlib/CategoryTheory/Presentable/EssentiallyLarge.lean

Statistics

Metric	Count
Definitions	0
Theorems exists_equivalence, essentiallyLarge_top	2
Total	2

CategoryTheory.HasCardinalFilteredGenerator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_equivalence 📖	mathematical	—	CategoryTheory.Category CategoryTheory.Equivalence	—	CategoryTheory.exists_equivalence_iff_of_locallySmall toLocallySmall exists_generator CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top

CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
essentiallyLarge_top 📖	mathematical	CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator	CategoryTheory.ObjectProperty.EssentiallySmall Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	CategoryTheory.ObjectProperty.instEssentiallySmallFullSubcategoryOfLocallySmallOfEssentiallySmall_1 CategoryTheory.ObjectProperty.instSmallOfObjOfSmall small_sigma UnivLE.small UnivLE.self small_subtype CategoryTheory.instSmallFunctorOfLocallySmall univLE_of_max CategoryTheory.locallySmall_of_univLE exists_colimitsOfShape CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_obj CategoryTheory.Limits.hasColimit_of_iso

---

← Back to Index