Theorem Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_card

Modification history

2025-05-18 18:58
Mathlib/SetTheory/Cardinal/Embedding.lean
feat(GroupTheory/GroupAction/MultiplePretransitivity): define multiply transitive actions (#23386) …
Added Fin.Embedding.exists_embedding_disjoint_range_of_add_le_ENat_cardView on Github →