pretopology_toGrothendieck — Mathlib

English

The pretopology associated to a space generates the Grothendieck topology of the space.

Русский

Препотопология пространства порождает Гротендикову топологию пространства.

LaTeX

$$$Opens.pretopology T \\text{ generates } Opens.grothendieckTopology T$$$

Lean4

/-- The pretopology associated to a space induces the Grothendieck topology associated to the space.
-/
@[simp]
theorem pretopology_toGrothendieck : (Opens.pretopology T).toGrothendieck = Opens.grothendieckTopology T :=
  by
  rw [← toPretopology_grothendieckTopology]
  apply (Pretopology.gi (Opens T)).l_u_eq

Похожие утверждения