Metamath Proof Explorer

Table of Contents - 18.5. Inner product (pre-Hilbert) spaces

1. Definition and basic properties
   1. ccphlo
   2. df-ph
   3. phnv
   4. phrel
   5. phnvi
   6. isphg
   7. phop
2. Examples of pre-Hilbert spaces
   1. cncph
   2. elimph
   3. elimphu
3. Properties of pre-Hilbert spaces
   1. isph
   2. phpar2
   3. phpar
   4. ip0i
   5. ip1ilem
   6. ip1i
   7. ip2i
   8. ipdirilem
   9. ipdiri
   10. ipasslem1
   11. ipasslem2
   12. ipasslem3
   13. ipasslem4
   14. ipasslem5
   15. ipasslem7
   16. ipasslem8
   17. ipasslem9
   18. ipasslem10
   19. ipasslem11
   20. ipassi
   21. dipdir
   22. dipdi
   23. ip2dii
   24. dipass
   25. dipassr
   26. dipassr2
   27. dipsubdir
   28. dipsubdi
   29. pythi
   30. siilem1
   31. siilem2
   32. siii
   33. sii
   34. ipblnfi
   35. ip2eqi
   36. phoeqi
   37. ajmoi
   38. ajfuni
   39. ajfun
   40. ajval