Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-21 14:25 5bc18a9e

View on Github →

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

Estimated changes