Commit 2021-01-25 17:49 1dfa81a1
View on Github →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.