LocallySmall

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

Statistics

Metric	Count
Definitions hasLocalizationOfLocallySmall, hasLocalizationOfLocallySmall'	2
Theorems hasLocalizationOfLocallySmall'_def, locallySmall_of_hasLocalization	2
Total	4

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
hasLocalizationOfLocallySmall 📖	CompOp	—
hasLocalizationOfLocallySmall' 📖	CompOp	1 math math: hasLocalizationOfLocallySmall'_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLocalizationOfLocallySmall'_def 📖	mathematical	—	hasLocalizationOfLocallySmall'	—	CategoryTheory.Localization.essSurj
locallySmall_of_hasLocalization 📖	mathematical	—	CategoryTheory.LocallySmall	—	small_of_injective instIsLocalizationLocalization'Q' CategoryTheory.instSmallHomOfLocallySmall CategoryTheory.locallySmall_of_univLE UnivLE.self CategoryTheory.Functor.map_injective CategoryTheory.Equivalence.faithful_functor

---

← Back to Index