instEffectiveEpiOfEffectiveEpiFamily

English

If f: X → B is a member of an effective epi family X → B indexed by α, then f is an effective epi.

Русский

Если f: X → B является компонентом эффективного эпиморфного семейства X → B, индексированного множества α, то f — эффективная эпиморфия.

LaTeX

$$$\operatorname{EffectiveEpiFamily} (X,\pi) \Rightarrow \operatorname{EffectiveEpi}(f)$$$

Lean4

instance {B X : C} (f : X ⟶ B) [EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f)] : EffectiveEpi f :=
  ⟨⟨effectiveEpiStructOfEffectiveEpiFamilySingleton f⟩⟩

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