mathlib

5bc18a9e - feat(topology/category/limits): Generalize Topological Kőnig's lemma (#7982)

feat(topology/category/limits): Generalize Topological Kőnig's lemma (#7982) This PR generalizes the Topological Kőnig's lemma to work with limits over cofiltered categories (as opposed to just directed orders). Along the way, we also prove some more API for the category instance on `ulift C`, and provide an `as_small C` construction for a category `C`. Coauthored with @kmill Co-authored-by: Kyle Miller <kmill31415@gmail.com>