Retraction characterization of lambda-injectivity (source code)

= Retraction characterization of lambda-injectivity
{title2=$PJ=I_X,\quad\|P\|\le\lambda$}

A space is a <lambda-injective normed space> exactly when every linear isometry $J:X\to Z$ has a bounded left inverse as displayed. Necessity extends the inverse on $J(X)$. For sufficiency, embed $X$ in <bounded scalar functions on an index set>, extend the composed operator coordinatewise, and compose that extension with the assumed left inverse. The associated operator $JP$ is a projection onto $J(X)$.