Theorems · Definition · category theory
CategoryTheory.ObjectProperty.Small
{C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ObjectProperty C → PropA property of objects is small relative to a universe w
if the corresponding subtype is.
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.Categorystatement and proof · cited by 32,673
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
- Smallproof · cited by 369
Cited by34
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_lestatement and proof · cited by 7
- CategoryTheory.ObjectProperty.EssentiallySmall.exists_small_le'statement · cited by 4
- CategoryTheory.ObjectProperty.EssentiallySmall.of_leproof · cited by 3
- CategoryTheory.hasInitial_of_isCoseparatingstatement and proof · cited by 2
- CategoryTheory.wellPowered_of_isDetectingstatement and proof · cited by 2
- CategoryTheory.ObjectProperty.IsStrongGenerator.isDense_colimitsCardinalClosure_ιstatement and proof · cited by 2
- CategoryTheory.Limits.hasColimits_of_hasLimits_of_isCoseparatingstatement and proof · cited by 1
- CategoryTheory.HasCardinalFilteredGenerator.exists_small_generatorstatement and proof · cited by 1
- CategoryTheory.Limits.hasLimits_of_hasColimits_of_isSeparatingstatement and proof · cited by 1
- CategoryTheory.IsCardinalLocallyPresentable.iff_exists_isStrongGeneratorstatement and proof · cited by 1
- CategoryTheory.hasTerminal_of_isSeparatingstatement and proof · cited by 1
- CommRingCat.essentiallySmall_of_finiteTypeproof · cited by 1