instIsCocontinuous — Mathlib

English

An instance asserting G is cocontinuous with respect to J and K, given the density and fullness hypotheses.

Русский

Экземпляр, утверждающий, что G когоплотна по отношению к J и K, при условии плотности и полноты.

LaTeX

$$$[G.IsCocontinuous J K]$$$

Lean4

instance (priority := 900) : G.IsCocontinuous J K where
  cover_lift
    hS :=
    letI := IsDenseSubsite.isCoverDense J K G
    letI := IsDenseSubsite.isLocallyFull J K G
    IsDenseSubsite.functorPushforward_mem_iff.mp (IsCoverDense.functorPullback_pushforward_covering ⟨_, hS⟩)

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