hasLimit_const_of_isConnected

Mathlib.CategoryTheory.Limits.Connected

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.hasLimit_const_of_isConnected

English

If J is connected, the constant functor (J ⥤ C) with value X has a limit.

Русский

Если J связно, константный функтор с значением X имеет предел.

LaTeX

$$$\mathrm{HasLimit}((\mathrm{Functor.const}\ J).\mathrm{obj}\ X)$$$

Lean4

instance hasLimit_const_of_isConnected : HasLimit ((Functor.const J).obj X) :=
  ⟨_, isLimitConstCone J X⟩

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

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

Разделы

Аффилиация

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