chore(analysis/convex/topology): split (#18187)
Split the facts about the topology of convex sets into two files, for topological vector spaces and normed spaces. This makes the former a more elementary file, as indeed it feels like it should be. It also slightly decreases the length of the longest path in mathlib.
