hasColimit_iff_of_iso — Mathlib

English

HasColimit F holds iff HasColimit G holds when F ≅ G.

Русский

Колимит F существует тогда и только тогда, когда существует колимит G, если F эквивалентен G.

LaTeX

$$$\\text{HasColimit } F \\iff \\text{HasColimit } G$ for $F \\cong G$$$

Lean4

theorem hasColimit_iff_of_iso {F G : J ⥤ C} (α : F ≅ G) : HasColimit F ↔ HasColimit G :=
  ⟨fun _ ↦ hasColimit_of_iso α.symm, fun _ ↦ hasColimit_of_iso α⟩

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