instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies

English

If F preserves finite effective epi families, then F preserves effective epis.

Русский

Если F сохраняет конечные эффективные эпиморфные семейства, то F сохраняет эффективные эпиморфии.

LaTeX

$$$[F.PreservesFiniteEffectiveEpiFamilies] \Rightarrow \operatorname{PreservesEffectiveEpis} F$$$

Lean4

instance (F : C ⥤ D) [PreservesEffectiveEpiFamilies.{0} F] : PreservesFiniteEffectiveEpiFamilies F where
  preserves _ _ := inferInstance

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