instHasLimits

Mathlib.Topology.Category.Compactum

URI: https://scilib.ai/kg/mathlib#Compactum.instHasLimits

English

Compactum has all limits (in the categorical sense).

Русский

Категория Compactum имеет все пределы.

LaTeX

$$$\\text{HasLimits}(\\text{Compactum})$$$

Lean4

instance : HasLimits Compactum :=
  hasLimits_of_hasLimits_createsLimits forget

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

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

Разделы

Аффилиация

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