Metamath Proof Explorer
Table of Contents - 10.9. Generalized pre-Hilbert and Hilbert spaces
- Definition and basic properties
- cphl
- cipf
- df-phl
- df-ipf
- isphl
- phllvec
- phllmod
- phlsrng
- phllmhm
- ipcl
- ipcj
- iporthcom
- ip0l
- ip0r
- ipeq0
- ipdir
- ipdi
- ip2di
- ipsubdir
- ipsubdi
- ip2subdi
- ipass
- ipassr
- ipassr2
- ipffval
- ipfval
- ipfeq
- ipffn
- phlipf
- ip2eq
- isphld
- phlpropd
- ssipeq
- phssipval
- phssip
- phlssphl
- Orthocomplements and closed subspaces
- cocv
- ccss
- cthl
- df-ocv
- df-css
- df-thl
- ocvfval
- ocvval
- elocv
- ocvi
- ocvss
- ocvocv
- ocvlss
- ocv2ss
- ocvin
- ocvsscon
- ocvlsp
- ocv0
- ocvz
- ocv1
- unocv
- iunocv
- cssval
- iscss
- cssi
- cssss
- iscss2
- ocvcss
- cssincl
- css0
- css1
- csslss
- lsmcss
- cssmre
- mrccss
- thlval
- thlbas
- thlbasOLD
- thlle
- thlleOLD
- thlleval
- thloc
- Orthogonal projection and orthonormal bases
- cpj
- chil
- cobs
- df-pj
- df-hil
- df-obs
- pjfval
- pjdm
- pjpm
- pjfval2
- pjval
- pjdm2
- pjff
- pjf
- pjf2
- pjfo
- pjcss
- ocvpj
- ishil
- ishil2
- isobs
- obsip
- obsipid
- obsrcl
- obsss
- obsne0
- obsocv
- obs2ocv
- obselocv
- obs2ss
- obslbs