Commit 2022-12-13 22:24 4a1bf948

View on Github →

feat(data/set/n_ary): Distributivity of ∩ (#17924) set.image2 f for injective2 f distributes over intersection. Also move the required results from data.set.prod to data.set.n_ary. As a bonus, this makes quite a few files not depend on data.set.n_ary anymore and matches the import direction for the corresponding finset files.

Estimated changes

Modified src/data/finset/n_ary.lean

added theorem finset.image₂_inter_left

added theorem finset.image₂_inter_right

Modified src/data/set/n_ary.lean

added theorem set.image2_curry

added theorem set.image2_inter_left

added theorem set.image2_inter_right

added theorem set.image2_mk_eq_prod

added theorem set.image_prod

added theorem set.image_uncurry_prod

Modified src/data/set/prod.lean

deleted theorem set.image2_curry

deleted theorem set.image2_mk_eq_prod

deleted theorem set.image_prod

deleted theorem set.image_uncurry_prod

Modified src/order/bounds/basic.lean