mathlib3

ea3815fb - feat(analysis/normed_space/inner_product): upgrade orthogonal projection to a continuous linear map (#5543)

feat(analysis/normed_space/inner_product): upgrade orthogonal projection to a continuous linear map (#5543) Upgrade the orthogonal projection, from a linear map `E →ₗ[𝕜] K` to a continuous linear map `E →L[𝕜] K`.