feat(analysis/convex/topology): minimize import

[ADedecker]

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.

---

[sgouezel]

bors d+

[bors[bot]]

:v: ADedecker can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[PatrickMassot]

bors merge

[bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests