Commit 2023-03-26 08:04 003bcd76

View on Github →

feat: port CategoryTheory.Sites.Pretopology (#3093)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Sites/Pretopology.lean

added def CategoryTheory.Pretopology.gi

added theorem CategoryTheory.Pretopology.le_def

added theorem CategoryTheory.Pretopology.mem_toGrothendieck

added def CategoryTheory.Pretopology.ofGrothendieck

added def CategoryTheory.Pretopology.toGrothendieck

added theorem CategoryTheory.Pretopology.toGrothendieck_bot

added def CategoryTheory.Pretopology.trivial

added structure CategoryTheory.Pretopology