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.





leanprover-community/mathlib,leanprover-community/mathlib