Inductive CategoryTheory.IsCofiltered.CofilteredClosure

Modification history

2023-09-08 11:01
Mathlib/CategoryTheory/Filtered/Small.lean
feat: a functor from a small category to a filtered category factors through a small filtered category (#6212)
Added CategoryTheory.IsCofiltered.CofilteredClosureView on Github →