iSup_eq_of_mem_grothendieck — Mathlib

English

The presieve obtained from coveringOfPresieve and then converted back via presieveOfCoveringAux yields the original presieve.

Русский

Полученная из coveringOfPresieve предшествуемая presieveOfCovering через presieveOfCoveringAux снова даёт исходный presieve.

LaTeX

$$$\\text{presieveOfCoveringAux}(\\text{coveringOfPresieve } Y R) Y = R$$$

Lean4

/-- If `R` is a presieve in the Grothendieck topology on `Opens X`, the covering family associated
to `R` really is _covering_, i.e. the union of all open sets equals `U`.
-/
theorem iSup_eq_of_mem_grothendieck (hR : Sieve.generate R ∈ Opens.grothendieckTopology X U) :
    iSup (coveringOfPresieve U R) = U := by
  apply le_antisymm
  · refine iSup_le ?_
    intro f
    exact f.2.1.le
  intro x hxU
  rw [Opens.coe_iSup, Set.mem_iUnion]
  obtain ⟨V, iVU, ⟨W, iVW, iWU, hiWU, -⟩, hxV⟩ := hR x hxU
  exact ⟨⟨W, ⟨iWU, hiWU⟩⟩, iVW.le hxV⟩

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