sheafifyOf — Mathlib

English

If a family f of local sections satisfies a predicate P, then its sheafified version satisfies the corresponding predicate P.sheafify.

Русский

Если множество локальных секций f удовлетворяет предикату P, то после простаивания через Sheafification, версия предиката P.sheafify тоже выполняется.

LaTeX

$$∃ f, P.pred f ⇒ P.sheafify.pred f$$

Lean4

theorem sheafifyOf {T : X → Type*} {P : PrelocalPredicate T} {U : Opens X} {f : ∀ x : U, T x} (h : P.pred f) :
    P.sheafify.pred f := fun x ↦ ⟨U, x.2, 𝟙 _, by convert h⟩

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