Commit 2024-10-18 16:28 7b3afdd0

View on Github →

feat: more lemmas about the size of pointwise sets (#17231) Complete the API and follow the convention that Cardinal.mk is called card and Nat.card is called natCard in lemma names. From LeanCamCombi

Estimated changes

added theorem Cardinal.mk_div_le
added theorem Cardinal.mk_inv
added theorem Cardinal.mk_mul_le
added theorem Cardinal.mk_smul_set
deleted theorem Set.card_div_le
deleted theorem Set.card_inv
deleted theorem Set.card_mul_le
deleted theorem Set.card_smul_set
added theorem Set.natCard_div_le
added theorem Set.natCard_inv
added theorem Set.natCard_mul_le
added theorem Set.natCard_smul_set
added theorem Cardinal.mk_image2_le
added theorem Cardinal.mk_setProd