Forget

📁 Source: Mathlib/Topology/Sheaves/Forget.lean

Statistics

Metric	Count
Definitions	0
Theorems isSheaf_iff_isSheaf_comp, isSheaf_iff_isSheaf_comp'	2
Total	2

TopCat.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSheaf_iff_isSheaf_comp 📖	mathematical	—	IsSheaf CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	—	isSheaf_iff_isSheaf_comp'
isSheaf_iff_isSheaf_comp' 📖	mathematical	—	IsSheaf CategoryTheory.Functor.comp Opposite TopologicalSpace.Opens TopCat.carrier TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder	—	CategoryTheory.Presheaf.isSheaf_iff_isSheaf_comp

---

← Back to Index