full_sheafPushforwardContinuous — Mathlib

English

The pushforward along G for presheaves is full when G is dense and locally full with continuity.

Русский

Пушфорвард по G полно, когда G плотный и локально полночный и непрерывный.

LaTeX

$$$(G.sheafPushforwardContinuous A J K).Full$$$

Lean4

instance full_sheafPushforwardContinuous : Full (G.sheafPushforwardContinuous A J K) :=
  letI := IsDenseSubsite.isCoverDense J K G
  letI := IsDenseSubsite.isLocallyFull J K G
  inferInstance

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