feat(analysis/convex/topology): minimize import (#16052)
Importing `analysis/normed_space/finite_dimension` was problematic for defining the strong operator topology because this needs quite a few facts about convexity but it has to be defined before `continuous_linear_map.has_op_norm`.
