Grothendieck topology on a topological space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Define the Grothendieck topology and the pretopology associated to a topological space, and show
that the pretopology induces the topology.
The covering (pre)sieves on
X are those for which the union of domains contains
site, Grothendieck topology, space
Implementation notes #
We define the two separately, rather than defining the Grothendieck topology as that generated
by the pretopology for the purpose of having nice definitional properties for the sieves.
The Grothendieck topology associated to a topological space.
The Grothendieck pretopology associated to a topological space.
The pretopology associated to a space is the largest pretopology that
generates the Grothendieck topology associated to the space.
The pretopology associated to a space induces the Grothendieck topology associated to the space.