Commit 2023-03-26 20:49 d010c13a

View on Github →

feat: port CategoryTheory.Sites.Spaces (#3111)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Spaces.lean

added def Opens.grothendieckTopology

added def Opens.pretopology

added theorem Opens.pretopology_ofGrothendieck

added theorem Opens.pretopology_toGrothendieck