mathlib3

1dfa81a1 - feat(analysis/normed_space/inner_product): double orthogonal complement is closure (#5876)

feat(analysis/normed_space/inner_product): double orthogonal complement is closure (#5876) Put a submodule structure on the closure (as a set in a topological space) of a submodule of a topological module. Show that in a complete inner product space, the double orthogonal complement of a submodule is its closure.