Metamath Proof Explorer

Table of Contents - 10.11. Generalized pre-Hilbert and Hilbert spaces

1. Definition and basic properties
   1. cphl
   2. cipf
   3. df-phl
   4. df-ipf
   5. isphl
   6. phllvec
   7. phllmod
   8. phlsrng
   9. phllmhm
   10. ipcl
   11. ipcj
   12. iporthcom
   13. ip0l
   14. ip0r
   15. ipeq0
   16. ipdir
   17. ipdi
   18. ip2di
   19. ipsubdir
   20. ipsubdi
   21. ip2subdi
   22. ipass
   23. ipassr
   24. ipassr2
   25. ipffval
   26. ipfval
   27. ipfeq
   28. ipffn
   29. phlipf
   30. ip2eq
   31. isphld
   32. phlpropd
   33. ssipeq
   34. phssipval
   35. phssip
   36. phlssphl
2. Orthocomplements and closed subspaces
   1. cocv
   2. ccss
   3. cthl
   4. df-ocv
   5. df-css
   6. df-thl
   7. ocvfval
   8. ocvval
   9. elocv
   10. ocvi
   11. ocvss
   12. ocvocv
   13. ocvlss
   14. ocv2ss
   15. ocvin
   16. ocvsscon
   17. ocvlsp
   18. ocv0
   19. ocvz
   20. ocv1
   21. unocv
   22. iunocv
   23. cssval
   24. iscss
   25. cssi
   26. cssss
   27. iscss2
   28. ocvcss
   29. cssincl
   30. css0
   31. css1
   32. csslss
   33. lsmcss
   34. cssmre
   35. mrccss
   36. thlval
   37. thlbas
   38. thlle
   39. thlleval
   40. thloc
3. Orthogonal projection and orthonormal bases
   1. cpj
   2. chil
   3. cobs
   4. df-pj
   5. df-hil
   6. df-obs
   7. pjfval
   8. pjdm
   9. pjpm
   10. pjfval2
   11. pjval
   12. pjdm2
   13. pjff
   14. pjf
   15. pjf2
   16. pjfo
   17. pjcss
   18. ocvpj
   19. ishil
   20. ishil2
   21. isobs
   22. obsip
   23. obsipid
   24. obsrcl
   25. obsss
   26. obsne0
   27. obsocv
   28. obs2ocv
   29. obselocv
   30. obs2ss
   31. obslbs