mathlib

37119b41 - feat(topology): normed spaces are (locally) path connected (#3689)