mathlib

19da20b0 - feat(combinatorics/hall): generalized Hall's Marriage Theorem (#7825)

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. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>