Theorem GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finite

Modification history

2024-07-31 21:06
Mathlib/Order/KonigLemma.lean
feat(Order/KonigLemma): Kőnig's infinity lemma (#12273) …
Added GradeMinOrder.exists_nat_orderEmbedding_of_forall_covby_finiteView on Github →