Commit 2023-01-19 20:37 bafc24af

View on Github →

feat: port Data.Fintype.Sum (#1679)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Sum.lean

added theorem Finset.exists_equiv_extend_of_card_eq

added theorem Finset.univ_disjSum_univ

added theorem Fintype.card_subtype_or

added theorem Fintype.card_subtype_or_disjoint

added theorem Fintype.card_sum

added theorem Set.MapsTo.exists_equiv_extend_of_card_eq

added def fintypeOfFintypeNe

added theorem image_subtype_ne_univ_eq_image_erase

added theorem image_subtype_univ_ssubset_image_univ

added theorem infinite_sum