mem_grothendieckTopology — Mathlib

English

The sieve generated by presieveOfCovering is a member of the Grothendieck topology on iSup U.

Русский

Сгенерированное presieveOfCovering сито принадлежит GrothendieckTopology над iSup U.

LaTeX

$$mem_grothendieckTopology$$

Lean4

/-- The sieve generated by `presieveOfCovering U` is a member of the Grothendieck topology.
-/
theorem mem_grothendieckTopology : Sieve.generate (presieveOfCovering U) ∈ Opens.grothendieckTopology X (iSup U) :=
  by
  intro x hx
  obtain ⟨i, hxi⟩ := Opens.mem_iSup.mp hx
  exact ⟨U i, Opens.leSupr U i, ⟨U i, 𝟙 _, Opens.leSupr U i, ⟨i, rfl⟩, Category.id_comp _⟩, hxi⟩

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