Commit 2022-04-29 14:39 7373832e

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.