Theorem RelEmbedding.toEmbedding_injective

Modification history

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