Commit 2022-07-11 14:26 611dccaf

View on Github →

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

Estimated changes

Modified src/analysis/inner_product_space/basic.lean

added def inner_product_space.is_self_adjoint.clm

added theorem inner_product_space.is_self_adjoint.clm_apply

added theorem inner_product_space.is_self_adjoint.continuous