instHasFiniteLimits

Mathlib.CategoryTheory.Sites.Limits

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Sheaf.instHasFiniteLimits

English

If D has finite limits, then HasFiniteLimits (Sheaf J D).

Русский

Если в D существуют конечные пределы, то в категории шейфов J D существуют конечные пределы.

LaTeX

$$$(\text{HasFiniteLimits } D) \Rightarrow (\text{HasFiniteLimits } (\mathrm{Sh}(J,D))).$$$

Lean4

instance [HasFiniteLimits D] : HasFiniteLimits (Sheaf J D) :=
  ⟨fun _ ↦ inferInstance⟩

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

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

Разделы

Аффилиация

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