English
The pretopology associated to a space is the largest pretopology that generates the Grothendieck topology associated to the space.
Русский
Препротопология пространства является наибольшей препротопологией, порождающей соответствующую Гротендикову топологию пространства.
LaTeX
$$$(Opens.pretopology T).toGrothendieck = Opens.grothendieckTopology T$$$
Lean4
/-- The pretopology associated to a space is the largest pretopology that
generates the Grothendieck topology associated to the space. -/
@[simp]
theorem toPretopology_grothendieckTopology : (Opens.grothendieckTopology T).toPretopology = Opens.pretopology T :=
by
apply le_antisymm
· intro X R hR x hx
rcases hR x hx with ⟨U, f, ⟨V, g₁, g₂, hg₂, _⟩, hU⟩
exact ⟨V, g₂, hg₂, g₁.le hU⟩
· intro X R hR x hx
rcases hR x hx with ⟨U, f, hf, hU⟩
exact ⟨U, f, Sieve.le_generate R U hf, hU⟩
