HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8782) |
Hilbert Space Explorer
(8783-10363) |
User Sandboxes
(10364-10725) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | hlimcaui 9101 | If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. |
         | ||
| Theorem | hlimcau 9102 | If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. |
  | ||
| Theorem | hlimunii 9103 | A Hilbert space sequence converges to at most one limit. |
  | ||
| Theorem | hlimuni 9104 | A Hilbert space sequence converges to at most one limit. |
|
| ||
| Theorem | hlimreu 9105 | The limit of a Hilbert space sequence is unique. |
     | ||
| Theorem | hlimeu 9106 | The limit of a Hilbert space sequence is unique. |
| | ||
| Theorem | chsscm 9107 | The hypothesis defines the set of complete subspaces of Hilbert space. A complete subspace is one in which every Cauchy sequence of vectors in the subspace converges to a member of the subspace (Definition of complete subspace in [Beran] p. 96). Any closed subspace of a Hilbert space is complete. Part of Remark 3.12 of [Beran] p. 107. |
         
   | ||
| Theorem | chcmh 9108 | The hypothesis defines the set of complete subspaces of Hilbert space (see chsscm 9107). A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107. |
|
| ||
| Theorem | ch2 9109 | A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107. |
|
| ||
| Theorem | chcompl 9110 | Completeness of a closed subspace of Hilbert space. |
|
| ||
| Theorem | helch 9111 | The unit Hilbert lattice element (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65. |
 | ||
| Theorem | helsh 9112 | Hilbert space is a subspace of Hilbert space. |
| | ||
| Theorem | shsspwh 9113 | Subspaces are subsets of Hilbert space. |
 | ||
| Theorem | chsspwh 9114 | Closed subspaces are subsets of Hilbert space. |
| | ||
| Theorem | hsn0elch 9115 | The zero subspace belongs to the set of closed subspaces of Hilbert space. |
| ||
| Theorem | norm1t 9116 | From any nonzero Hilbert space vector, construct a vector whose norm is 1. |
     | ||
| Theorem | norm1ex 9117 | A normalized vector exists in a subspace iff the subspace has a non-zero vector. |
 | ||
| Theorem | norm1hext 9118 | A normalized vector can exist only iff the Hilbert space has a non-zero vector. |
|
| ||
| Orthocomplements | ||
| Definition | df-oc 9119 |
Define orthogonal complement of a subset (usually a subspace) of
Hilbert space. The orthogonal complement is the set of all vectors
orthogonal to all vectors in the subset. See ocvalt 9148 and chocval 9166
for its value. Textbooks usually denote this unary operation with the
symbol  as a
small superscript, although Mittelstaedt uses
the symbol as a prefix operation. Here we define a function (prefix
operation)
rather than introducing a new syntactical form.
This lets us take advantage of the theorems about functions that we
already have proved under set theory. Definition of [Mittelstaedt]
p. 9.
|
  
  | ||
| Definition | df-ch0 9120 | Define the zero for closed subspaces of Hilbert space. See h0elch 9122 for closure law. |
 | ||
| Theorem | elch0 9121 | Membership in zero for closed subspaces of Hilbert space. |
|
| ||
| Theorem | h0elch 9122 | The zero subspace is a closed subspace. Part of Proposition 1 of [Kalmbach] p. 65. |
| | ||
| Theorem | h0elsh 9123 | The zero subspace is a subspace of Hilbert space. |
| | ||
| Theorem | hhssva 9124 | The vector addition operation on a subspace. |
    
 | ||
| Theorem | hhsssm 9125 | The scalar multiplication operation on a subspace. |
 | ||
| Theorem | hhssnm 9126 | The norm operation on a subspace. |
 | ||
| Theorem | hhssabl 9127 | Abelian group property of subspace addition. |
|
Abel | ||
| Theorem | hhssablt 9128 | Abelian group property of subspace addition. |
|
Abel | ||
| Theorem | hhssnv 9129 | Normed complex vector space property of a subspace. |
|
NrmCVec | ||
| Theorem | hhssnvt 9130 | Normed complex vector space property of a subspace. |
|
NrmCVec | ||
| Theorem | hhsst 9131 |
A member of is a
subspace.
|
SubSp | ||
| Theorem | hhshsslem1 9132 | Lemma for hhsssh 9134. |
| Theorem | hhshsslem2 9133 | Lemma for hhsssh 9134. |
| Theorem | hhsssh 9134 |
The predicate " is
a subspace of Hilbert space."
|
|
SubSp | ||
| Theorem | hhsssh2 9135 |
The predicate " is
a subspace of Hilbert space."
|
|
NrmCVec | ||
| Theorem | hhssba 9136 | The base set of a subspace. |
|
Base | ||
| Theorem | hhssvs 9137 | The vector subtraction operation on a subspace. |
  | ||
| Theorem | hhssvsf 9138 | Mapping of the vector subtraction operation on a subspace. |
|
| ||
| Theorem | hhssph 9139 | Inner product space property of a subspace. |
|
CPreHil | ||
| Theorem | hhssims 9140 | Induced metric of a subspace. |
 
IndMet | ||
| Theorem | hhssims2 9141 | Induced metric of a subspace. |
|
IndMet
| ||
| Theorem | hhssmet 9142 | Induced metric of a subspace. |
|
IndMet Met | ||
| Theorem | hhssmetba 9143 | The base set for the metric of a subspace. |
IndMet 
| ||
| Theorem | hhssmetdval 9144 | Value of the distance function of the metric space of a subspace. |
|
IndMet
| ||
| Theorem | hhsscms 9145 | The induced metric of a closed subspace is complete. |
|
IndMet CMet | ||
| Theorem | hhssbn 9146 | Banach space property of a closed subspace. |
|
CBan | ||
| Theorem | hhsshl 9147 | Hilbert space property of a closed subspace. |
|
CHil | ||
| Theorem | ocvalt 9148 | Value of orthogonal complement of a subset of Hilbert space. |
|
| ||
| Theorem | ocelt 9149 | Membership in orthogonal complement of H subset. |
| | ||