isColimit_exists_rep — Mathlib

English

For a colimit D of F, every element x in D.pt is the image of some representative y from some F.obj j.

Русский

Для колимита D диаграммы F каждый элемент x в D.pt является образом некоторого элемента y из некоторого объекта F.obj j.

LaTeX

$$$\\exists j\\exists y:\\,\\, D.ι.app j y = x$$$

Lean4

theorem isColimit_exists_rep {D : Cocone F} (hD : IsColimit D) (x : ToType D.pt) :
    ∃ (j : J) (y : ToType (F.obj j)), D.ι.app j y = x :=
  by
  obtain ⟨a, rfl⟩ := Concrete.from_union_surjective_of_isColimit F hD x
  exact ⟨a.1, a.2, rfl⟩

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