instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies

English

For any F, if F preserves finite effective epi families then F preserves effective epis.

Русский

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

LaTeX

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

Lean4

instance (F : C ⥤ D) [PreservesFiniteEffectiveEpiFamilies F] : PreservesEffectiveEpis F where
  preserves _ := inferInstance

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