Theorem Opens.pretopology_toGrothendieck

Modification history

2023-03-26 20:49
Mathlib/CategoryTheory/Sites/Spaces.lean
feat: port CategoryTheory.Sites.Spaces (#3111)
Added Opens.pretopology_toGrothendieckView on Github →