instEffectiveEpiFamilyOfIsIsoDesc

English

If HasCoproduct X and Sigma.desc π is an isomorphism, then X π is an effective epi family.

Русский

Если есть копродукт X и Sigma.desc π является изоморфизмом, то X π образует эффективное эпиморфное семейство.

LaTeX

$$$\operatorname{HasCoproduct}(X) \wedge \operatorname{IsIso}(\Sigma.\mathrm{desc}\ \pi) \Rightarrow \operatorname{EffectiveEpiFamily} X\pi$$$

Lean4

instance {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [IsIso (Sigma.desc π)] :
    EffectiveEpiFamily X π :=
  ⟨⟨effectiveEpiFamilyStructOfIsIsoDesc X π⟩⟩

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