mathlib
611dccaf - feat(analysis/inner_product_space): the Hellinger-Toeplitz theorem (#15055)

Commit

3 years ago

feat(analysis/inner_product_space): the Hellinger-Toeplitz theorem (#15055) Prove the Hellinger-Toeplitz theorem as a corollary of the closed graph theorem.

Author

mcdoll

Parents

0980bacb

mathlib 611dccaf - feat(analysis/inner_product_space): the Hellinger-Toeplitz theorem (#15055)

mathlib
611dccaf - feat(analysis/inner_product_space): the Hellinger-Toeplitz theorem (#15055)