Commit 2021-06-12 02:37 2d175ae6

View on Github →

feat(topology/category/Top/limits): Kőnig's lemma for fintypes (#6288) Specializes Top.nonempty_limit_cone_of_compact_t2_inverse_system to an inverse system of nonempty fintypes.

Estimated changes

Modified src/topology/category/Top/limits.lean

added theorem nonempty_sections_of_fintype_inverse_system.init

added theorem nonempty_sections_of_fintype_inverse_system

added def ulift.directed_order