instEffectiveEpiFamily — Mathlib

English

Let C be a category and f: X → B an effective epi. Then the singleton family consisting of X over B via f is an effective epi family.

Русский

Пусть C — категория и f: X → B является эффективной эпиморфией. Тогда единичное семейство, содержащее X и отображающее f к B, является эффективным эпиморфическим семейством.

LaTeX

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

Lean4

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

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