LocallySmall

📁 Source: Mathlib/CategoryTheory/Comma/LocallySmall.lean

Statistics

Metric	Count
Definitions	0
Theorems locallySmall, locallySmall, locallySmall, locallySmall, locallySmall	5
Total	5

CategoryTheory.Comma

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall CategoryTheory.Comma CategoryTheory.commaCategory	—	small_of_injective small_prod CategoryTheory.instSmallHomOfLocallySmall hom_ext

CategoryTheory.CostructuredArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall CategoryTheory.CostructuredArrow CategoryTheory.instCategoryCostructuredArrow	—	CategoryTheory.Comma.locallySmall CategoryTheory.locallySmall_of_thin CategoryTheory.Discrete.instSubsingletonDiscreteHom

CategoryTheory.Over

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall CategoryTheory.Over CategoryTheory.instCategoryOver	—	CategoryTheory.CostructuredArrow.locallySmall

CategoryTheory.StructuredArrow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.Comma.locallySmall CategoryTheory.locallySmall_of_thin CategoryTheory.Discrete.instSubsingletonDiscreteHom

CategoryTheory.Under

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallySmall 📖	mathematical	—	CategoryTheory.LocallySmall CategoryTheory.Under CategoryTheory.instCategoryUnder	—	CategoryTheory.StructuredArrow.locallySmall

---

← Back to Index