Metamath Proof Explorer

Table of Contents - 18.7. Complex Hilbert spaces

1. Definition and basic properties
   1. chlo
   2. df-hlo
   3. ishlo
   4. hlobn
   5. hlph
   6. hlrel
   7. hlnv
   8. hlnvi
   9. hlvc
   10. hlcmet
   11. hlmet
   12. hlpar2
   13. hlpar
2. Standard axioms for a complex Hilbert space
   1. hlex
   2. hladdf
   3. hlcom
   4. hlass
   5. hl0cl
   6. hladdid
   7. hlmulf
   8. hlmulid
   9. hlmulass
   10. hldi
   11. hldir
   12. hlmul0
   13. hlipf
   14. hlipcj
   15. hlipdir
   16. hlipass
   17. hlipgt0
   18. hlcompl
3. Examples of complex Hilbert spaces
   1. cnchl
4. Hellinger-Toeplitz Theorem
   1. htthlem
   2. htth