Commit 2024-10-04 10:12 6d453919

View on Github →

feat(Data/Finset): right elements of a finset in the sum type (#17014)

Estimated changes

Modified Mathlib/Data/Finset/Preimage.lean

added theorem Finset.preimage_inl

added theorem Finset.preimage_inr

Modified Mathlib/Data/Finset/Sum.lean

added theorem Finset.Injective2_disjSum

added theorem Finset.card_toLeft_add_card_toRight

added theorem Finset.card_toLeft_le

added theorem Finset.card_toRight_le

added theorem Finset.disjSum_eq_iff

added theorem Finset.disjSum_inj

added theorem Finset.eq_disjSum_iff

added theorem Finset.mem_toLeft

added theorem Finset.mem_toRight

added def Finset.toLeft

added theorem Finset.toLeft_cons_inl

added theorem Finset.toLeft_cons_inr

added theorem Finset.toLeft_disjSum

added theorem Finset.toLeft_disjSum_toRight

added theorem Finset.toLeft_image_swap

added theorem Finset.toLeft_insert_inl

added theorem Finset.toLeft_insert_inr

added theorem Finset.toLeft_inter

added theorem Finset.toLeft_map_sumComm

added theorem Finset.toLeft_monotone

added theorem Finset.toLeft_sdiff

added theorem Finset.toLeft_subset_toLeft

added theorem Finset.toLeft_union

added def Finset.toRight

added theorem Finset.toRight_cons_inl

added theorem Finset.toRight_cons_inr

added theorem Finset.toRight_disjSum

added theorem Finset.toRight_image_swap

added theorem Finset.toRight_insert_inl

added theorem Finset.toRight_insert_inr

added theorem Finset.toRight_inter

added theorem Finset.toRight_map_sumComm

added theorem Finset.toRight_monotone

added theorem Finset.toRight_sdiff

added theorem Finset.toRight_subset_toRight

added theorem Finset.toRight_union