instEffectiveEpiEffectiveEpiOver — Mathlib

English

If F is effectively enough, then for any X in D, the morphism F.effectiveEpiOver X is an effective epi.

Русский

Если F обладает свойством effectively enough, то для любого X в D отображение F.effectiveEpiOver X является эффективной эпиморфией.

LaTeX

$$$[F.EffectivelyEnough] \Rightarrow \operatorname{EffectiveEpi}\big(F.\mathrm{effectiveEpiOver} X\big)$$$

Lean4

instance (X : D) : EffectiveEpi (F.effectiveEpiOver X) :=
  (EffectivelyEnough.presentation X).some.effectiveEpi

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