coverPreserving — Mathlib

English

An instance of the previous result specialized to a particular coherent functor that preserves covers densely.

Русский

Специализация предыдущего результата на конкретный когерентный функтор, сохраняющий покрытия плотным образом.

LaTeX

$$coverPreserving$$

Lean4

theorem coverPreserving :
    haveI := F.reflects_precoherent
    CoverPreserving (coherentTopology _) (coherentTopology _) F :=
  IsDenseSubsite.coverPreserving _ _ _

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