mathlib3
3c93c656 - feat(analysis/inner_product_space/l2_space): the family of subspaces spanned by finitely many elements of a Hilbert basis has dense supremum (#15821)

Commit
3 years ago
feat(analysis/inner_product_space/l2_space): the family of subspaces spanned by finitely many elements of a Hilbert basis has dense supremum (#15821)
Author
Parents
Loading