mathlib

f00007dc - feat(analysis/normed_space/pointwise): more on pointwise operations on sets in normed spaces (#10820)

feat(analysis/normed_space/pointwise): more on pointwise operations on sets in normed spaces (#10820) Also move all related results to a new file `analysis/normed_space/pointwise`, to shorten `normed_space/basic` a little bit.