Metamath Proof Explorer

Table of Contents - 19.2. Inner product and norms

1. Inner product
   1. his5
   2. his52
   3. his35
   4. his35i
   5. his7
   6. hiassdi
   7. his2sub
   8. his2sub2
   9. hire
   10. hiidrcl
   11. hi01
   12. hi02
   13. hiidge0
   14. his6
   15. his1i
   16. abshicom
   17. hial0
   18. hial02
   19. hisubcomi
   20. hi2eq
   21. hial2eq
   22. hial2eq2
   23. orthcom
   24. normlem0
   25. normlem1
   26. normlem2
   27. normlem3
   28. normlem4
   29. normlem5
   30. normlem6
   31. normlem7
   32. normlem8
   33. normlem9
   34. normlem7tALT
   35. bcseqi
   36. normlem9at
2. Norms
   1. dfhnorm2
   2. normf
   3. normval
   4. normcl
   5. normge0
   6. normgt0
   7. norm0
   8. norm-i
   9. normne0
   10. normcli
   11. normsqi
   12. norm-i-i
   13. normsq
   14. normsub0i
   15. normsub0
   16. norm-ii-i
   17. norm-ii
   18. norm-iii-i
   19. norm-iii
   20. normsubi
   21. normpythi
   22. normsub
   23. normneg
   24. normpyth
   25. normpyc
   26. norm3difi
   27. norm3adifii
   28. norm3lem
   29. norm3dif
   30. norm3dif2
   31. norm3lemt
   32. norm3adifi
   33. normpari
   34. normpar
   35. normpar2i
   36. polid2i
   37. polidi
   38. polid
3. Relate Hilbert space to normed complex vector spaces
   1. hilablo
   2. hilid
   3. hilvc
   4. hilnormi
   5. hilhhi
   6. hhnv
   7. hhva
   8. hhba
   9. hh0v
   10. hhsm
   11. hhvs
   12. hhnm
   13. hhims
   14. hhims2
   15. hhmet
   16. hhxmet
   17. hhmetdval
   18. hhip
   19. hhph
4. Bunjakovaskij-Cauchy-Schwarz inequality
   1. bcsiALT
   2. bcsiHIL
   3. bcs
   4. bcs2
   5. bcs3