coveringOfPresieve_apply — Mathlib

English

If U is a family of opens, the presieve on iSup U generated by presieveOfCovering U is a covering presieve in the grothendieck topology on iSup U.

Русский

Если U — семейство открытых подмножеств, то порожденный presieveOfCovering U на iSup U является покрывающим presieve вGrothendieckTopology на iSup U.

LaTeX

$$$\\mathrm{iSup\\!}\\;\\text{Covering presieve} = \\text{presieveOfCovering } U$$$

Lean4

@[simp]
theorem coveringOfPresieve_apply (U : Opens X) (R : Presieve U) (f : Σ V, { f : V ⟶ U // R f }) :
    coveringOfPresieve U R f = f.1 :=
  rfl

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