instHasFiniteLimits

Mathlib.CategoryTheory.Galois.Basic

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

English

If C is a PreGaloisCategory, then C has finite limits.

Русский

Если C — предгалойская категория, то у C есть конечные пределы.

LaTeX

$$$HasFiniteLimits(C)$, given $PreGaloisCategory(C)$.$$

Lean4

instance : HasFiniteLimits C :=
  hasFiniteLimits_of_hasTerminal_and_pullbacks

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

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

Разделы

Аффилиация

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