mathlib

f48c65aa - feat(analysis/convex/topology): connectedness and `same_ray` (#16661)

feat(analysis/convex/topology): connectedness and `same_ray` (#16661) Add lemmas that the set of vectors in the same ray as a given vector, and the set of nonzero vectors in the same ray as a given nonzero vector, are connected (in a real normed space).