hasLimit

Mathlib.CategoryTheory.Limits.Constructions.EventuallyConstant

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsEventuallyConstantTo.hasLimit

English

If F is eventually constant to i0 and J is cofiltered, then F has a limit.

Русский

Если F является в конечном счёте константной к i0 и J кофильтрована, то F имеет предел.

LaTeX

$$$\text{HasLimit}(F)$$$

Lean4

theorem hasLimit : HasLimit F :=
  ⟨_, h.isLimitCone⟩

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

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

Разделы

Аффилиация

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