Def TopCat.Sheaf.isTerminalOfEmpty

Modification history

2026-03-06 08:34

Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

refactor(CategoryTheory/Sites): redefine the category of sheaves using `ObjectProperty.FullSubcategory` (#36081) …

Modified TopCat.Sheaf.isTerminalOfEmpty View on Github →

2023-05-21 12:23

Mathlib/Topology/Sheaves/SheafCondition/Sites.lean

feat: port Topology.Sheaves.SheafCondition.Sites (#4150)

Added TopCat.Sheaf.isTerminalOfEmpty View on Github →