Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-13 17:27 96dc1f71

View on Github →

chore(data/fintype/basic): generalize some lemmas to Sort* (#17503) Also add function.embedding.nonempty_iff_card_le.

Estimated changes

Modified src/data/fintype/basic.lean

added theorem function.embedding.nonempty_iff_card_le

modified theorem infinite.of_injective

modified theorem infinite.of_surjective

modified theorem not_surjective_finite_infinite