mk — Mathlib · SciLib

Lean4
/-- This definition provides a convenient way to show that a multifork is a limit. -/
@[simps]
def mk (lift : ∀ E : Multifork I, E.pt ⟶ K.pt) (fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i)
    (uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ i : J.L, m ≫ K.ι i = E.ι i) → m = lift E) : IsLimit K :=
  { lift
    fac := by
      rintro E (a | b)
      · apply fac
      · rw [← E.w (WalkingMulticospan.Hom.fst b), ← K.w (WalkingMulticospan.Hom.fst b), ← Category.assoc]
        congr 1
        apply fac
    uniq := by
      rintro E m hm
      apply uniq
      intro i
      apply hm }
Похожие утверждения