mathlib documentation

category_theory.limits.filtered

Possession of filtered colimits #

@[class]

Class for having all cofiltered limits of a given size.

Instances of this typeclass
@[class]

Class for having all filtered colimits of a given size.

Instances of this typeclass