of_hasFiniteColimits

Mathlib.CategoryTheory.Filtered.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsFiltered.of_hasFiniteColimits

English

If a category C has finite colimits, then C is filtered.

Русский

Если у категории C есть конечные колимиты, то C является фильтрованной.

LaTeX

$$$[\\text{HasFiniteColimits } C] \\\\Rightarrow \\\\operatorname{IsFiltered}(C).$$$

Lean4

theorem of_hasFiniteColimits [HasFiniteColimits C] : IsFiltered C :=
  of_cocone_nonempty.{v} C fun F => ⟨colimit.cocone F⟩

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

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

Разделы

Аффилиация

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