effectiveEpi_iff_effectiveEpiFamily

English

For any B and X with f : X → B, EffectiveEpi f is equivalent to EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f).

Русский

Для любых B и X с f: X → B эквивалентно EffectiveEpi f и EffectiveEpiFamily (единичное семейство) X с f.

LaTeX

$$$\operatorname{EffectiveEpi}(f) \iff \operatorname{EffectiveEpiFamily}(\lambda u:\,\mathrm{Unit}. X)(\lambda u:\,\mathrm{Unit}. f)$$$

Lean4

theorem effectiveEpi_iff_effectiveEpiFamily {B X : C} (f : X ⟶ B) :
    EffectiveEpi f ↔ EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f) :=
  ⟨fun _ ↦ inferInstance, fun _ ↦ inferInstance⟩

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