isColimit_iff_coconeTypesIsColimit

English

Variant of the previous criterion: for c : CoconeTypes F, there is an equivalence c.IsColimit ⇔ Nonempty IsColimit (F.coconeTypesEquiv c).

Русский

Вариант предыдущего критерия: для c : CoconeTypes F верно c.IsColimit ⇔ Nonempty IsColimit (F.coconeTypesEquiv c).

LaTeX

$$$$ c.IsColimit \iff Nonempty\ (IsColimit\ ( F.coconeTypesEquiv\ c )). $$$$

Lean4

theorem isColimit_iff_coconeTypesIsColimit {F : J ⥤ Type u} (c : Cocone F) :
    Nonempty (IsColimit c) ↔ (F.coconeTypesEquiv.symm c).IsColimit := by
  simp only [Functor.CoconeTypes.isColimit_iff, Equiv.apply_symm_apply]

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