HomeUnicode version.
| Home |
Metamath Proof Explorer | < Previous Next > |
| Browser slow? Try the
Unicode version. |
| Color key: | Metamath Proof Explorer
(1-8787) |
Hilbert Space Explorer
(8788-10368) |
User Sandboxes
(10369-10781) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | chssi 9101 | A closed subspace of a Hilbert space is a subset of Hilbert space. |
       | ||
| Theorem | chel 9102 | A member of a closed subspace of a Hilbert space is a vector. |
    | ||
| Theorem | cheli 9103 | A member of a closed subspace of a Hilbert space is a vector. |
 | ||
| Theorem | chlim 9104 | The limit property of a closed subspace of a Hilbert space. |
       | ||
| Theorem | hlim0 9105 | The zero sequence in Hilbert space converges to the zero vector. |
   | ||
| Theorem | hlimcaui 9106 | If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. |
 | ||
| Theorem | hlimcau 9107 | If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. |
|
| ||
| Theorem | hlimunii 9108 | A Hilbert space sequence converges to at most one limit. |
 | ||
| Theorem | hlimuni 9109 | A Hilbert space sequence converges to at most one limit. |
|
| ||
| Theorem | hlimreu 9110 | The limit of a Hilbert space sequence is unique. |
    | ||
| Theorem | hlimeu 9111 | The limit of a Hilbert space sequence is unique. |
| | ||
| Theorem | chsscm 9112 | 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 9113 | The hypothesis defines the set of complete subspaces of Hilbert space (see chsscm 9112). A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107. |
|
| ||
| Theorem | ch2 9114 | A Hilbert subspace is closed iff it is complete. Remark 3.12(C) of [Beran] p. 107. |
|
| ||
| Theorem | chcompl 9115 | Completeness of a closed subspace of Hilbert space. |
|
| ||
| Theorem | helch 9116 | 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 9117 | Hilbert space is a subspace of Hilbert space. |
| | ||
| Theorem | shsspwh 9118 | Subspaces are subsets of Hilbert space. |
 | ||
| Theorem | chsspwh 9119 | Closed subspaces are subsets of Hilbert space. |
| | ||
| Theorem | hsn0elch 9120 | The zero subspace belongs to the set of closed subspaces of Hilbert space. |
|
| ||
| Theorem | norm1t 9121 | From any nonzero Hilbert space vector, construct a vector whose norm is 1. |
     | ||
| Theorem | norm1ex 9122 | A normalized vector exists in a subspace iff the subspace has a non-zero vector. |
 | ||
| Theorem | norm1hext 9123 | A normalized vector can exist only iff the Hilbert space has a non-zero vector. |
|
| ||
| Orthocomplements | ||
| Definition | df-oc 9124 |
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 9153 and chocval 9171
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 9125 | Define the zero for closed subspaces of Hilbert space. See h0elch 9127 for closure law. |
 | ||
| Theorem | elch0 9126 | Membership in zero for closed subspaces of Hilbert space. |
|
| ||
| Theorem | h0elch 9127 | The zero subspace is a closed subspace. Part of Proposition 1 of [Kalmbach] p. 65. |
| | ||
| Theorem | h0elsh 9128 | The zero subspace is a subspace of Hilbert space. |
| | ||
| Theorem | hhssva 9129 | The vector addition operation on a subspace. |
   
 | ||
| Theorem | hhsssm 9130 | The scalar multiplication operation on a subspace. |
 | ||
| Theorem | hhssnm 9131 | The norm operation on a subspace. |
 | ||
| Theorem | hhssabl 9132 | Abelian group property of subspace addition. |
|
Abel | ||
| Theorem | hhssablt 9133 | Abelian group property of subspace addition. |
|
Abel | ||
| Theorem | hhssnv 9134 | Normed complex vector space property of a subspace. |
|
NrmCVec | ||
| Theorem | hhssnvt 9135 | Normed complex vector space property of a subspace. |
|
NrmCVec | ||
| Theorem | hhsst 9136 |
A member of is a
subspace.
|
SubSp | ||
| Theorem | hhshsslem1 9137 | Lemma for hhsssh 9139. |
| Theorem | hhshsslem2 9138 | Lemma for hhsssh 9139. |
| Theorem | hhsssh 9139 |
The predicate " is
a subspace of Hilbert space."
|
|
SubSp | ||
| Theorem | hhsssh2 9140 |
The predicate " is
a subspace of Hilbert space."
|
|
NrmCVec | ||
| Theorem | hhssba 9141 | The base set of a subspace. |
|
Base | ||
| Theorem | hhssvs 9142 | The vector subtraction operation on a subspace. |
  | ||
| Theorem | hhssvsf 9143 | Mapping of the vector subtraction operation on a subspace. |
|
| ||
| Theorem | hhssph 9144 | Inner product space property of a subspace. |
|
CPreHil | ||
| Theorem | hhssims 9145 | Induced metric of a subspace. |
 
IndMet | ||
| Theorem | hhssims2 9146 | Induced metric of a subspace. |
|
IndMet
| ||
| Theorem | hhssmet 9147 | Induced metric of a subspace. |
|
IndMet Met | ||
| Theorem | hhssmetba 9148 | The base set for the metric of a subspace. |
IndMet 
| ||
| Theorem | hhssmetdval 9149 | Value of the distance function of the metric space of a subspace. |
|
IndMet
| ||
| Theorem | hhsscms 9150 | The induced metric of a closed subspace is complete. |
|
IndMet CMet | ||
| Theorem | hhssbn 9151 | Banach space property of a closed subspace. |
|
| ||