effectiveEpiStructOfEffectiveEpiFamilySingleton

Lean4

/-- A single element `EffectiveEpiFamily` consists of an `EffectiveEpi`
-/
noncomputable def effectiveEpiStructOfEffectiveEpiFamilySingleton {B X : C} (f : X ⟶ B)
    [EffectiveEpiFamily (fun () ↦ X) (fun () ↦ f)] : EffectiveEpiStruct f
    where
  desc e h := EffectiveEpiFamily.desc (fun () ↦ X) (fun () ↦ f) (fun () ↦ e) (fun _ _ g₁ g₂ hg ↦ h g₁ g₂ hg)
  fac e h := EffectiveEpiFamily.fac (fun () ↦ X) (fun () ↦ f) (fun () ↦ e) (fun _ _ g₁ g₂ hg ↦ h g₁ g₂ hg) ()
  uniq e h m
    hm := EffectiveEpiFamily.uniq (fun () ↦ X) (fun () ↦ f) (fun () ↦ e) (fun _ _ g₁ g₂ hg ↦ h g₁ g₂ hg) m (fun _ ↦ hm)

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