mem_toGrothendieck_sieves_of_superset

English

If R is a presieve covering a given object X in K, and R ≤ S, then S belongs to the Grothendieck topology associated to K at X.

Русский

Если R — покрывающая предзева для X в K, и R ⊆ S, тогда S принадлежит топологии Гротендика, связанной с K в X.

LaTeX

$$$$ (R \le S) \wedge (R \in K X) \Rightarrow S \in K.toGrothendieck X $$$$

Lean4

/-- Any sieve that contains a covering presieve for a coverage is a covering sieve for the associated
Grothendieck topology.
-/
theorem mem_toGrothendieck_sieves_of_superset (K : Coverage C) {X : C} {S : Sieve X} {R : Presieve X} (h : R ≤ S)
    (hR : R ∈ K X) : S ∈ K.toGrothendieck X :=
  K.saturate_of_superset ((Sieve.generate_le_iff _ _).mpr h) (Coverage.Saturate.of X _ hR)

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