mathlib

4dd7ecae - feat(analysis/{seminorm, convex/specific_functions}): A seminorm is convex (#10203)

feat(analysis/{seminorm, convex/specific_functions}): A seminorm is convex (#10203) This proves `seminorm.convex_on`, `convex_on_norm` (which is morally a special case of the former) and leverages it to golf `seminorm.convex_ball`. This also fixes the explicitness of arguments of `convex_on.translate_left` and friends.