Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-23 22:18 88c79e57

View on Github →

feat(data/fintype/basic): embeddings of fintypes based on cardinal inequalities (#9346) From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/mapping.20a.20fintype.20into.20a.20finset/near/254493754, based on suggestions by @kmill and @eric-wieser and @riccardobrasca.

Estimated changes

Modified src/data/fintype/basic.lean

modified theorem function.embedding.equiv_of_fintype_self_embedding_to_embedding

added theorem function.embedding.exists_of_card_le_finset

modified theorem function.embedding.is_empty_of_card_lt

added theorem function.embedding.nonempty_of_card_le

added def function.embedding.trunc_of_card_le