IsSmall

📁 Source: Mathlib/CategoryTheory/MorphismProperty/IsSmall.lean

Statistics

Metric	Count
Definitions IsSmall	1
Theorems small_toSet, isSmall_iff_eq_ofHoms, isSmall_ofHoms	3
Total	4

CategoryTheory.MorphismProperty

Definitions

Name	Category	Theorems
IsSmall 📖	CompData	5 math math: isSmall_iff_eq_ofHoms, isSmall_ofHoms, CategoryTheory.IsGrothendieckAbelian.instIsSmallGeneratingMonomorphismsOfSmallSubobject, IsCardinalForSmallObjectArgument.isSmall, CategoryTheory.SmallObject.isSmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSmall_iff_eq_ofHoms 📖	mathematical	—	IsSmall ofHoms	—	IsSmall.small_toSet ext ofHoms_iff CategoryTheory.Arrow.mk_eq Equiv.symm_apply_apply arrow_mk_mem_toSet_iff isSmall_ofHoms small_self
isSmall_ofHoms 📖	mathematical	—	IsSmall ofHoms	—	small_of_surjective

CategoryTheory.MorphismProperty.IsSmall

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
small_toSet 📖	mathematical	—	Small Set.Elem CategoryTheory.Arrow CategoryTheory.MorphismProperty.toSet	—	—

---

← Back to Index