Theorems · Definition · category theory
CategoryTheory.ObjectProperty
(C : Type u) → [CategoryTheory.CategoryStruct.{v, u} C] → Type uA property of objects in a category C is a predicate C → Prop.
- Cited by
- 798 results in Mathlib
- Foundations
- Depth 1 from the axioms, rests on 2 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CategoryTheory.CategoryStructstatement and proof · cited by 343
Cited by1,149
Results whose statement or proof uses this declaration.
- CategoryTheory.ObjectProperty.FullSubcategory.objstatement and proof · cited by 1,316
- CategoryTheory.ObjectProperty.FullSubcategorystatement · cited by 726
- CategoryTheory.Over.isMonostatement · cited by 111
- CategoryTheory.ObjectProperty.ιstatement and proof · cited by 95
- CategoryTheory.Functor.essImagestatement · cited by 82
- CategoryTheory.ObjectProperty.FullSubcategory.propertystatement and proof · cited by 76
- CategoryTheory.ObjectProperty.homMkstatement and proof · cited by 71
- CategoryTheory.ObjectProperty.IsClosedUnderIsomorphismsstatement · cited by 68
- CategoryTheory.ObjectProperty.IsSerreClassstatement · cited by 61
- CategoryTheory.ObjectProperty.isoClosurestatement and proof · cited by 61
- ModuleCat.isFGstatement · cited by 53
- CategoryTheory.ObjectProperty.isoModSerrestatement and proof · cited by 50
Showing the 200 most cited of 1,149.