Commit 2024-07-31 21:06 e6d4b051

feat(Order/KonigLemma): Kőnig's infinity lemma (#12273) This PR proves Kőnig's infinity lemma in terms of covers in a strongly atomic order, and it gives a common formulation for directed systems, which is useful for applications such as Ramsey theory. One of the things we needed is a Fintype instance for RelEmbedding r s. This would have caused a bad diamond with SimpleGraph.Hom.instFintype, so instead we remove the latter and provide their common generalization RelHom.instFintype in Fintype.Pi.