locallyCoverDense_of_isCoverDense

English

If G is locally dense with respect to K, then it satisfies the locally dense condition as an object-level property, i.e., there is a local-factorization/density condition relative to K across G.

Русский

Если G локально плотен относительно K, то выполняется локальная слабая плотность для G в отношении K.

LaTeX

$$$[G.\\mathrm{IsLocallyDense } K] \\Rightarrow G.\\mathrm{LocallyCoverDense } K$$$

Lean4

instance (priority := 900) locallyCoverDense_of_isCoverDense [G.IsCoverDense K] : G.LocallyCoverDense K where
  functorPushforward_functorPullback_mem _ _ := IsCoverDense.functorPullback_pushforward_covering _

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