Opens.pretopology_ofGrothendieck
theorem Opens.pretopology_ofGrothendieck :
∀ (T : Type u) [inst : TopologicalSpace T],
CategoryTheory.Pretopology.ofGrothendieck (TopologicalSpace.Opens T) (Opens.grothendieckTopology T) =
Opens.pretopology T
The theorem `Opens.pretopology_ofGrothendieck` states that for any topological space `T`, the pretopology associated with this space is the largest possible pretopology that generates the Grothendieck topology associated with the same space `T`. In other words, this theorem establishes a connection between the Grothendieck topology and the pretopology of a given topological space, showing that the pretopology is the maximal one that can give rise to the specific Grothendieck topology.
More concisely: The pretopology of a topological space is the largest pretopology generating its associated Grothendieck topology.
|
Opens.pretopology_toGrothendieck
theorem Opens.pretopology_toGrothendieck :
∀ (T : Type u) [inst : TopologicalSpace T],
CategoryTheory.Pretopology.toGrothendieck (TopologicalSpace.Opens T) (Opens.pretopology T) =
Opens.grothendieckTopology T
This theorem states that for any type `T` endowed with a topological space structure, the Grothendieck topology associated to the space `T` is induced by the pretopology associated to the same space. In other words, the conversion of the pretopology of a given space `T` to a Grothendieck topology yields the same Grothendieck topology as directly defined on the space `T`.
More concisely: The Grothendieck topology on a topological space `T` is equal to the topology induced by its pretopology.
|