SheafOfFunctions

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

Statistics

Metric	Count
Definitions sheafToType, sheafToTypes	2
Theorems toType_isSheaf, toTypes_isSheaf	2
Total	4

TopCat

Definitions

Name	Category	Theorems
sheafToType 📖	CompOp	—
sheafToTypes 📖	CompOp	—

TopCat.Presheaf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toType_isSheaf 📖	mathematical	—	IsSheaf CategoryTheory.types TopCat.presheafToType	—	toTypes_isSheaf
toTypes_isSheaf 📖	mathematical	—	IsSheaf CategoryTheory.types TopCat.presheafToTypes	—	isSheaf_of_isSheafUniqueGluing_types TopologicalSpace.Opens.mem_iSup

---

← Back to Index