Def Opens.grothendieckTopology

Modification history

2024-02-09 22:56
Mathlib/CategoryTheory/Sites/Spaces.lean
chore: tidy various files (#10362)
Modified Opens.grothendieckTopologyView on Github →
2023-03-26 20:49
Mathlib/CategoryTheory/Sites/Spaces.lean
feat: port CategoryTheory.Sites.Spaces (#3111)
Added Opens.grothendieckTopologyView on Github →