Commit 2023-01-16 19:11 d93c09aa

View on Github →

feat: port Data.Finset.Sum (#1601)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Sum.lean

added theorem Finset.card_disjSum

added def Finset.disjSum

added theorem Finset.disjSum_empty

added theorem Finset.disjSum_mono

added theorem Finset.disjSum_mono_left

added theorem Finset.disjSum_mono_right

added theorem Finset.disjSum_ssubset_disjSum_of_ssubset_of_subset

added theorem Finset.disjSum_ssubset_disjSum_of_subset_of_ssubset

added theorem Finset.disjSum_strictMono_left

added theorem Finset.disj_sum_strictMono_right

added theorem Finset.disjoint_map_inl_map_inr

added theorem Finset.empty_disjSum

added theorem Finset.inl_mem_disjSum

added theorem Finset.inr_mem_disjSum

added theorem Finset.map_inl_disj_union_map_inr

added theorem Finset.mem_disjSum

added theorem Finset.val_disjSum