feat(analysis/convex/side): connectedness of sides (#16938)
Add lemmas that, in a real normed space, the sets of points on the same side of an affine subspace as a given point, or on the opposite side from a given point, are connected (or, under weaker conditions, preconnected).
