Metamath Proof Explorer
Table of Contents - 19.4. Subspaces and projections
- Subspaces
- df-sh
- issh
- issh2
- shss
- shel
- shex
- shssii
- sheli
- shelii
- sh0
- shaddcl
- shmulcl
- issh3
- shsubcl
- Closed subspaces
- df-ch
- isch
- isch2
- chsh
- chsssh
- chex
- chshii
- ch0
- chss
- chel
- chssii
- cheli
- chelii
- chlimi
- hlim0
- hlimcaui
- hlimf
- hlimuni
- hlimreui
- hlimeui
- isch3
- chcompl
- helch
- ifchhv
- helsh
- shsspwh
- chsspwh
- hsn0elch
- norm1
- norm1exi
- norm1hex
- Orthocomplements
- df-oc
- df-ch0
- elch0
- h0elch
- h0elsh
- hhssva
- hhsssm
- hhssnm
- issubgoilem
- hhssabloilem
- hhssabloi
- hhssablo
- hhssnv
- hhssnvt
- hhsst
- hhshsslem1
- hhshsslem2
- hhsssh
- hhsssh2
- hhssba
- hhssvs
- hhssvsf
- hhssims
- hhssims2
- hhssmet
- hhssmetdval
- hhsscms
- hhssbnOLD
- ocval
- ocel
- shocel
- ocsh
- shocsh
- ocss
- shocss
- occon
- occon2
- occon2i
- oc0
- ocorth
- shocorth
- ococss
- shococss
- shorth
- ocin
- occon3
- ocnel
- chocvali
- shuni
- chocunii
- pjhthmo
- occllem
- occl
- shoccl
- choccl
- choccli
- Subspace sum, span, lattice join, lattice supremum
- df-shs
- df-span
- df-chj
- df-chsup
- shsval
- shsss
- shsel
- shsel3
- shseli
- shscli
- shscl
- shscom
- shsva
- shsel1
- shsel2
- shsvs
- shsub1
- shsub2
- choc0
- choc1
- chocnul
- shintcli
- shintcl
- chintcli
- chintcl
- spanval
- hsupval
- chsupval
- spancl
- elspancl
- shsupcl
- hsupcl
- chsupcl
- hsupss
- chsupss
- hsupunss
- chsupunss
- spanss2
- shsupunss
- spanid
- spanss
- spanssoc
- sshjval
- shjval
- chjval
- chjvali
- sshjval3
- sshjcl
- shjcl
- chjcl
- shjcom
- shless
- shlej1
- shlej2
- shincli
- shscomi
- shsvai
- shsel1i
- shsel2i
- shsvsi
- shunssi
- shunssji
- shsleji
- shjcomi
- shsub1i
- shsub2i
- shub1i
- shjcli
- shjshcli
- shlessi
- shlej1i
- shlej2i
- shslej
- shincl
- shub1
- shub2
- shsidmi
- shslubi
- shlesb1i
- shsval2i
- shsval3i
- shmodsi
- shmodi
- Projection theorem
- pjhthlem1
- pjhthlem2
- pjhth
- pjhtheu
- Projectors
- df-pjh
- pjhfval
- pjhval
- pjpreeq
- pjeq
- axpjcl
- pjhcl