exists_coeq — Mathlib

English

If Initial F holds and C is IsCofilteredOrEmpty, then for any d and c with s,s' : F.obj c ⟶ d there exists c' and t : c' ⟶ c such that F.map t ≫ s = F.map t ≫ s'.

Русский

Если F начальнен и C — IsCofilteredOrEmpty, то для любых d, c и стрел s,s' : F.obj c ⟶ d существует c' и t : c' ⟶ c, такое что F.map t ≫ s = F.map t ≫ s'.

LaTeX

$$$\\text{Initial}(F) \\Rightarrow \\forall d,c\\ (s,s' : F.obj c \\to d), \\exists c',t: c' \\to c, F.map t \\circ s = F.map t \\circ s'$$$

Lean4

theorem exists_coeq [IsFilteredOrEmpty C] [Final F] {d : D} {c : C} (s s' : d ⟶ F.obj c) :
    ∃ (c' : C) (t : c ⟶ c'), s ≫ F.map t = s' ≫ F.map t :=
  ((final_iff_of_isFiltered F).1 inferInstance).2 s s'

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