mathlib3 documentation

category_theory.limits.filtered

Possession of filtered colimits #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[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