Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-08-10 09:04 e2521c31

View on Github →

feat(data/set/finite): card_image_of_injective and other minor lemmas (#245)

Estimated changes

Modified data/finset.lean

added theorem finset.coe_ssubset

Modified data/set/basic.lean

added theorem set.ssubset_iff_subset_not_subset

Modified data/set/finite.lean

added theorem finset.coe_to_finset'

added theorem set.card_image_of_inj_on

added theorem set.card_image_of_injective

added theorem set.card_lt_card