Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-02 04:59 19483ae3

View on Github →

feat(data/finset): inj on of image card eq (#6785)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.card_image_eq_iff_inj_on

modified theorem finset.image_val_of_inj_on

added theorem finset.inj_on_of_card_image_eq

Modified src/data/list/nodup.lean

added theorem list.inj_on_of_nodup_map

added theorem list.nodup_map_iff_inj_on

Modified src/data/multiset/nodup.lean

added theorem multiset.inj_on_of_nodup_map

added theorem multiset.nodup_map_iff_inj_on