instIsCofilteredULift — Mathlib

English

If a category C is cofiltered, then the lifted category ULift C is also cofiltered.

Русский

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

LaTeX

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

Lean4

instance [IsCofiltered C] : IsCofiltered (ULift.{u₂} C) :=
  IsCofiltered.of_equivalence ULift.equivalence

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