Documentation Verification Report

PresheafOfFunctions

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

Statistics

Metric	Count
Definitions `presheafToTop`, `presheafToType`, `presheafToTypes`	3
Theorems `presheafToTop_obj`, `presheafToType_map`, `presheafToType_obj`, `presheafToTypes_map`, `presheafToTypes_obj`	5
Total	8

TopCat

Definitions

Name	Category	Theorems
`presheafToTop` 📖	CompOp	1 math math: `presheafToTop_obj`
`presheafToType` 📖	CompOp	3 math math: `presheafToType_map`, `presheafToType_obj`, `Presheaf.toType_isSheaf`
`presheafToTypes` 📖	CompOp	3 math math: `presheafToTypes_map`, `Presheaf.toTypes_isSheaf`, `presheafToTypes_obj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`presheafToTop_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `presheafToTop` `Quiver.Hom` `TopCat` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `instCategory` `TopologicalSpace.Opens.toTopCat` `Opposite.unop`	—	—
`presheafToType_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `presheafToType` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `Opposite.unop` `DFunLike.coe` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `TopologicalSpace.Opens.opensHom.instFunLike` `Quiver.Hom.unop`	—	—
`presheafToType_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `presheafToType`	—	—
`presheafToTypes_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `Opposite` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `presheafToTypes` `DFunLike.coe` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Opposite.unop` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `TopologicalSpace.Opens.opensHom.instFunLike` `Quiver.Hom.unop`	—	—
`presheafToTypes_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `carrier` `str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `presheafToTypes`	—	—

---

← Back to Index