mathlib

c82be35d - feat(analysis/normed_space/inner_product): orthogonal complement lemmas (#5474)

feat(analysis/normed_space/inner_product): orthogonal complement lemmas (#5474) The orthogonal complement of a subspace is closed. The orthogonal complement of the orthogonal complement of a complete subspace is itself.