Commit 2021-10-13 21:29 19da20b0

feat(combinatorics/hall): generalized Hall's Marriage Theorem (#7825) Used the generalized Kőnig's lemma to prove a version of Hall's Marriage Theorem with the fintype constraint on the index type removed. The original fintype version is moved into hall/finite.lean, and the infinite version is put in hall/basic.lean. They are in separate files because the infinite version pulls in topology.category.Top.limits, which is a rather large dependency.