Theorems · Theorem · category theory
CategoryTheory.ObjectProperty.FullSubcategory.property
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C}
(self : P.FullSubcategory), P self.objThe predicate satisfied by all objects in this subcategory
- Cited by
- 76 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
- Assumes
- CategoryTheory.Category
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
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.ObjectProperty.FullSubcategory.objstatement · cited by 1,316
- CategoryTheory.ObjectPropertystatement and proof · cited by 798
- CategoryTheory.ObjectProperty.FullSubcategorystatement and proof · cited by 726
Cited by77
Results whose statement or proof uses this declaration.
- CategoryTheory.Functor.op_comp_isSheafproof · cited by 8
- CategoryTheory.Sheaf.isSeparatedproof · cited by 8
- TopCat.Sheaf.existsUnique_gluingproof · cited by 5
- CategoryTheory.sheafificationAdjunction_counit_app_valstatement and proof · cited by 4
- CategoryTheory.Sieve.forallYonedaIsSheaf_iff_colimitproof · cited by 4
- CategoryTheory.Functor.op_comp_isSheaf_of_typesproof · cited by 4
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage_compproof · cited by 4
- CategoryTheory.Functor.IsDenseSubsite.mapPreimage_map_of_facproof · cited by 4
- CategoryTheory.Functor.isContinuous_of_coverPreservingproof · cited by 4
- CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_mapproof · cited by 3