instHasColimits

Mathlib.Algebra.Category.ModuleCat.Topology.Basic

URI: https://scilib.ai/kg/mathlib#TopModuleCat.instHasColimits

English

TopModuleCat R has all small colimits.

Русский

TopModuleCat R имеет все малые колимиты.

LaTeX

$$$\\text{HasColimits }(\\mathrm{TopModuleCat}\\;R)$$$

Lean4

instance : HasColimits (TopModuleCat.{v} R) where

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

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

Разделы

Аффилиация

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