Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-27 17:20 99acfda0

View on Github →

feat(category_theory/sites): pretopology (#4648) Adds pretopologies.

Estimated changes

Created src/category_theory/sites/pretopology.lean

added def category_theory.pretopology.gi

added theorem category_theory.pretopology.mem_to_grothendieck

added def category_theory.pretopology.of_grothendieck

added def category_theory.pretopology.to_grothendieck

added theorem category_theory.pretopology.to_grothendieck_bot

added def category_theory.pretopology.trivial

added structure category_theory.pretopology

added def category_theory.pullback_arrows

added theorem category_theory.pullback_arrows_comm

added theorem category_theory.pullback_singleton