Commit 2021-01-02 00:36 ea3815fb

View on Github →

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.

Estimated changes

Modified src/analysis/normed_space/inner_product.lean

modified def orthogonal_projection

added theorem orthogonal_projection_fn_norm_sq

added theorem orthogonal_projection_norm_le

Modified src/geometry/euclidean/basic.lean