instIsFilteredULiftHom

Mathlib.CategoryTheory.Filtered.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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