Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-11-01 10:44 a477dfd3

View on Github →

feat(data/finite/card): Cardinality of union, image, and range (#17253) This PR adds lemmas for the cardinality of union, image, and range.

Estimated changes

added theorem finite.card_image_le
added theorem finite.card_range_le
modified theorem finite.card_subtype_le
modified theorem finite.card_subtype_lt
added theorem finite.cast_card_eq_mk
added theorem set.card_union_le