instHasFiniteLimitsLightCondMod

Mathlib.Condensed.Light.Limits

URI: https://scilib.ai/kg/mathlib#instHasFiniteLimitsLightCondMod

English

LightCondMod has finite limits.

Русский

LightCondMod имеет конечные пределы.

LaTeX

$$$\text{HasFiniteLimits LightCondMod}$$$

Lean4

instance : HasFiniteLimits (LightCondMod.{u} R) :=
  hasFiniteLimits_of_hasLimitsOfSize _

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

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

Разделы

Аффилиация

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