mathlib3

feat(analysis/normed_space/lp_space): "functoriality" of `lp`

#15754

Open