exists_colimitPresentation_diag_obj_iso

English

For j in h.J X there exists i and an isomorphism between (h.colimitPresentation X).diag.obj j and G i.

Русский

Для каждого j из h.J X существует i и изоморфизм между (h.colimitPresentation X).diag.obj j и G i.

LaTeX

$$$\exists i:\; ι,\; \text{Nonempty}((h.colimitPresentation X).diag.obj j \cong G i)$$$

Lean4

theorem exists_colimitPresentation_diag_obj_iso (j : h.J X) :
    ∃ (i : ι), Nonempty ((h.colimitPresentation X).diag.obj j ≅ G i) :=
  (h.exists_colimitPresentation X).choose_spec.choose_spec.choose_spec.choose_spec j

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