Commit 2023-01-20 23:55 a63928c3

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.