Inductive CategoryTheory.IsFiltered.FilteredClosure

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.IsFiltered.FilteredClosureView on Github →