instIsCofilteredULiftHom

Mathlib.CategoryTheory.Filtered.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instIsCofilteredULiftHom

English

If the base category C is cofilted, then ULiftHom C is cofilted.

Русский

Если категория C кофильтрована, то ULiftHom C кофильтрована.

LaTeX

$$$\\mathrm{IsCofiltered}(C) \\Rightarrow \\mathrm{IsCofiltered}(\\mathrm{ULiftHom}\\,C)$$$

Lean4

instance [IsCofiltered C] : IsCofiltered (ULiftHom C) :=
  IsCofiltered.of_equivalence ULiftHom.equiv

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

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

Разделы

Аффилиация

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