Theorem maximal_orthonormal_iff_dense_span
Modification history
2022-01-20 10:32
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space/l2): a Hilbert space is isometrically isomorphic to `ℓ²` (#11255) …
Deleted maximal_orthonormal_iff_dense_spanView on Github →