instHasLimitOfIsEventuallyConstant

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCofiltered.instHasLimitOfIsEventuallyConstant

English

Same as above: for an IsColimit cocone, each c.ι.app j is an isomorphism.

Русский

То же самое: для колимитного конуса каждый c.ι.app j — изоморфизм.

LaTeX

$$IsIso(c.ι.app j)$$

Lean4

instance [hF : IsEventuallyConstant F] [IsCofiltered J] : HasLimit F :=
  by
  obtain ⟨j, h⟩ := hF.exists_isEventuallyConstantTo
  exact h.hasLimit

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru