Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes