of_hasFiniteLimits

Mathlib.CategoryTheory.Filtered.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsCofiltered.of_hasFiniteLimits

English

If C has all finite limits, then C is cofiltered.

Русский

Если в C существуют все конечные пределы, то C - кофильтрована.

LaTeX

$$$[HasFiniteLimits\ C] \Rightarrow \mathrm{IsCofiltered} C$$$

Lean4

theorem of_hasFiniteLimits [HasFiniteLimits C] : IsCofiltered C :=
  of_cone_nonempty.{v} C fun F => ⟨limit.cone F⟩

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

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

Разделы

Аффилиация

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