mathlib3

7373832e - chore(analysis/convex): move `convex_on_norm`, change API (#13631)

chore(analysis/convex): move `convex_on_norm`, change API (#13631) * Move `convex_on_norm` from `specific_functions` to `topology`, use it to golf the proof of `convex_on_dist`. * The old `convex_on_norm` is now called `convex_on_univ_norm`. The new `convex_on_norm` is about convexity on any convex set. * Add `convex_on_univ_dist` and make `s : set E` an implicit argument in `convex_on_dist`. This way APIs about convexity of norm and distance agree.