A punctured open ball in a real normed space is homotopy equivalent to the unit sphere

Let $E$ be a real normed vector space, let $c\in E$ and let $r>0$. The punctured open ball $B(c,r)\setminus\{c\}$, with the subspace topology, is homotopy equivalent to the unit sphere $S(E)=\{u\in E:\|u\|=1\}$:

A homotopy equivalence is given by radial projection $y\mapsto (y-c)/\|y-c\|$, with homotopy inverse the inclusion $u\mapsto c+\tfrac r2\,u$ of the sphere of radius $r/2$ about $c$; the composite on the punctured ball is homotopic to the identity through the radial deformation $y\mapsto c+\bigl((1-t)\tfrac r2+t\|y-c\|\bigr)\,\frac{y-c}{\|y-c\|}$, $t\in[0,1]$, which stays in the punctured ball. This is the deformation retraction of $\mathbb R^n\setminus\{0\}$ onto $S^{n-1}$ (Hatcher, Chapter 0, Exercise 2), restricted to a ball and stated for an arbitrary real normed space. Its role here is to transport simple connectivity from the sphere to punctured coordinate balls in a manifold: a punctured coordinate ball in an $n$-manifold, $n\ge3$, is simply connected because $S^{n-1}$ is.

Formalization Note The statement is Nonempty (ContinuousMap.HomotopyEquiv ↥(Metric.ball c r \ {c}) ↥(Metric.sphere (0 : E) 1)), Mathlib's notion of homotopy equivalence between the two subtypes. No finite-dimensionality or inner-product structure is assumed on E.