instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite

Mathlib.Topology.Category.CompHausLike.Limits

URI: https://scilib.ai/kg/mathlib#CompHausLike.instHasColimitsOfShapeDiscreteOfHasExplicitFiniteCoproductsOfFinite

← MathLib Explorer

English

There are finite coproducts in CompHausLike P: HasFiniteCoproducts (CompHausLike P).

Русский

Существуют конечные копроизведения в CompHausLike P.

LaTeX

$$$\\text{HasFiniteCoproducts}(\\mathrm{CompHausLike} P)$$$

Lean4

instance [HasExplicitFiniteCoproducts.{w} P] (α : Type w) [Finite α] : HasColimitsOfShape (Discrete α) (CompHausLike P)
    where has_colimit _ := hasColimit_of_iso Discrete.natIsoFunctor

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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