SubcanonicalOver

Statistics

Name	Kind	Assumes	Proves	Validates	Depends On
`subcanonical_over` 📖	mathematical	—	`Subcanonical` `CategoryTheory.Over` `CategoryTheory.instCategoryOver` `over`	—	`Subcanonical.of_isSheaf_yoneda_obj` `CategoryTheory.Sieve.exists_eq_ofArrows` `CategoryTheory.Over.w` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Over.OverMorphism.ext` `Subcanonical.isSheaf_of_isRepresentable` `CategoryTheory.Functor.instIsRepresentableObjOppositeTypeYoneda` `CategoryTheory.Presieve.map_ofArrows` `CategoryTheory.Sieve.generate_sieve` `CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward` `CategoryTheory.Sieve.overEquiv_generate` `CategoryTheory.Sieve.ofArrows.eq_1` `mem_over_iff` `CategoryTheory.Presieve.FamilyOfElements.Compatible.sieveExtend` `CategoryTheory.Presieve.Arrows.Compatible.familyOfElements_compatible` `CategoryTheory.Presieve.IsSeparatedFor.ext` `CategoryTheory.Presieve.IsSheafFor.isSeparatedFor` `CategoryTheory.Sieve.le_generate` `CategoryTheory.Presieve.extend_agrees` `CategoryTheory.Presieve.FamilyOfElements.comp_of_compatible` `CategoryTheory.Sieve.downward_closed`

---