Commit 2025-06-05 11:03 c5cfb59c

View on Github →

feat(Data/Set/Image): Sum.elim lemmas (#22964) This PR adds some Sum.elim lemmas for images and preimages of sets. Used in #22137.

Estimated changes

Modified Mathlib/Data/Set/Image.lean

modified theorem Set.compl_compl_image

added theorem Set.disjoint_image_inl_image_inr

added theorem Set.disjoint_image_inl_range_inr

added theorem Set.disjoint_range_inl_image_inr

added theorem Set.image_sumElim

modified theorem Set.mem_compl_image

modified theorem Set.preimage_compl_eq_image_compl

added theorem Set.preimage_sumElim

modified theorem Set.range_inter_ssubset_iff_preimage_ssubset