Commit 2025-03-31 14:24 1cc7fcf3

View on Github →

feat(Finset): extra toLeft/toRight API (#23020) Add the API that I independently came up with in https://github.com/leanprover-community/mathlib4/pull/20433#issuecomment-2607541838.

Estimated changes

Modified Mathlib/Data/Finset/Sum.lean

modified theorem Finset.card_toLeft_add_card_toRight

modified theorem Finset.card_toLeft_le

modified theorem Finset.card_toRight_le

added theorem Finset.disjSum_subset

added theorem Finset.gc_map_inl_toLeft

added theorem Finset.gc_map_inr_toRight

added theorem Finset.map_inl_subset_iff_subset_toLeft

added theorem Finset.map_inr_subset_iff_subset_toRight

modified theorem Finset.mem_toLeft

modified theorem Finset.mem_toRight

added theorem Finset.subset_disjSum

added theorem Finset.subset_map_inl

added theorem Finset.subset_map_inr

modified def Finset.toLeft

modified def Finset.toRight

Modified Mathlib/Data/Fintype/Sum.lean

added theorem Finset.toLeft_eq_empty

added theorem Finset.toLeft_eq_univ

added theorem Finset.toLeft_univ

added theorem Finset.toRight_eq_empty

added theorem Finset.toRight_eq_univ

added theorem Finset.toRight_univ

modified theorem Finset.univ_disjSum_univ