Def CategoryTheory.GrothendieckTopology.closureOperator

Modification history

2023-05-31 05:42

Mathlib/CategoryTheory/Sites/Closed.lean

feat: port CategoryTheory.Sites.Closed (#3356)

Added CategoryTheory.GrothendieckTopology.closureOperator View on Github →