# Commit 2024-07-31 21:06 e6d4b051

View on Github →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`

.