mathlib

8187142b - feat(data/finset/pointwise): `s • t` is the union of the `a • t` (#14696)

feat(data/finset/pointwise): `s • t` is the union of the `a • t` (#14696) and a few other results leading to it. Also tag `set.coe_bUnion` with `norm_cast` and rename `finset.image_mul_prod`/`finset.add_image_prod` to `finset.image_mul_product`/`finset.image_add_product`