Documentation Verification Report

Points

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

Statistics

Metric	Count
Definitions `instSmallPointOpensGrothendieckTopologyPointsGrothendieckTopology`, `pointGrothendieckTopology`, `pointGrothendieckTopologyHomEquiv`, `pointsGrothendieckTopology`	4
Theorems `instHasEnoughPointsOpensGrothendieckTopology`, `instIsThinPointOpensGrothendieckTopology`, `instSubsingletonObjOpensFiber`, `isConservativeFamilyOfPoints_pointsGrothendieckTopology`	4
Total	8

Opens

Definitions

Name	Category	Theorems
`instSmallPointOpensGrothendieckTopologyPointsGrothendieckTopology` 📖	CompOp	—
`pointGrothendieckTopology` 📖	CompOp	—
`pointGrothendieckTopologyHomEquiv` 📖	CompOp	—
`pointsGrothendieckTopology` 📖	CompOp	1 math math: `isConservativeFamilyOfPoints_pointsGrothendieckTopology`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasEnoughPointsOpensGrothendieckTopology` 📖	mathematical	—	`CategoryTheory.GrothendieckTopology.HasEnoughPoints` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `grothendieckTopology`	—	`isConservativeFamilyOfPoints_pointsGrothendieckTopology`
`instIsThinPointOpensGrothendieckTopology` 📖	mathematical	—	`Quiver.IsThin` `CategoryTheory.GrothendieckTopology.Point` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `grothendieckTopology` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.GrothendieckTopology.Point.instCategory`	—	`CategoryTheory.GrothendieckTopology.Point.hom_ext` `CategoryTheory.NatTrans.ext'` `CategoryTheory.types_ext` `instSubsingletonObjOpensFiber`
`instSubsingletonObjOpensFiber` 📖	mathematical	—	`CategoryTheory.Functor.obj` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `CategoryTheory.types` `CategoryTheory.GrothendieckTopology.Point.fiber` `grothendieckTopology`	—	`CategoryTheory.GrothendieckTopology.Point.subsingleton_fiber_obj` `CategoryTheory.locallySmall_of_thin` `Preorder.subsingleton_hom` `le_top` `CategoryTheory.instMonoOfIsThin`
`isConservativeFamilyOfPoints_pointsGrothendieckTopology` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints` `TopologicalSpace.Opens` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `grothendieckTopology` `pointsGrothendieckTopology`	—	`CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'` `CategoryTheory.locallySmall_of_thin` `Preorder.subsingleton_hom` `CategoryTheory.instHasSheafifyType`

---

← Back to Index