Home | Metamath
Proof Explorer Theorem List (p. 281 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | normneg 28001 | The norm of a vector equals the norm of its negative. (Contributed by NM, 23-May-2005.) (New usage is discouraged.) |
Theorem | normpyth 28002 | Analogy to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
Theorem | normpyc 28003 | Corollary to Pythagorean theorem for orthogonal vectors. Remark 3.4(C) of [Beran] p. 98. (Contributed by NM, 26-Oct-1999.) (New usage is discouraged.) |
Theorem | norm3difi 28004 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
Theorem | norm3adifii 28005 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 30-Sep-1999.) (New usage is discouraged.) |
Theorem | norm3lem 28006 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
Theorem | norm3dif 28007 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 20-Apr-2006.) (New usage is discouraged.) |
Theorem | norm3dif2 28008 | Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
Theorem | norm3lemt 28009 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
Theorem | norm3adifi 28010 | Norm of differences around common element. Part of Lemma 3.6 of [Beran] p. 101. (Contributed by NM, 3-Oct-1999.) (New usage is discouraged.) |
Theorem | normpari 28011 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
Theorem | normpar 28012 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
Theorem | normpar2i 28013 | Corollary of parallelogram law for norms. Part of Lemma 3.6 of [Beran] p. 100. (Contributed by NM, 5-Oct-1999.) (New usage is discouraged.) |
Theorem | polid2i 28014 | Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
Theorem | polidi 28015 | Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of axiom ax-his3 27941. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
Theorem | polid 28016 | Polarization identity. Recovers inner product from norm. Exercise 4(a) of [ReedSimon] p. 63. The outermost operation is + instead of - due to our mathematicians' (rather than physicists') version of axiom ax-his3 27941. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Theorem | hilablo 28017 | Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
Theorem | hilid 28018 | The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007.) (New usage is discouraged.) |
GId | ||
Theorem | hilvc 28019 | Hilbert space is a complex vector space. Vector addition is , and scalar product is . (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
Theorem | hilnormi 28020 | Hilbert space norm in terms of vector space norm. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
CV | ||
Theorem | hilhhi 28021 | Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhnv 28022 | Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Theorem | hhva 28023 | The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Theorem | hhba 28024 | The base set of Hilbert space. This theorem provides an independent proof of df-hba 27826 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Theorem | hh0v 28025 | The zero vector of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | hhsm 28026 | The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Theorem | hhvs 28027 | The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
Theorem | hhnm 28028 | The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
CV | ||
Theorem | hhims 28029 | The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
Theorem | hhims2 28030 | Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhmet 28031 | The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhxmet 28032 | The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
Theorem | hhmetdval 28033 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhip 28034 | The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
Theorem | hhph 28035 | The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
Theorem | bcsiALT 28036 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | bcsiHIL 28037 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Proved from ZFC version.) (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
Theorem | bcs 28038 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
Theorem | bcs2 28039 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 28037. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
Theorem | bcs3 28040 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 28037. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
Theorem | hcau 28041* | Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hcauseq 28042 | A Cauchy sequences on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hcaucvg 28043* | A Cauchy sequence on a Hilbert space converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | seq1hcau 28044* | A sequence on a Hilbert space is a Cauchy sequence if it converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlimi 28045* | Express the predicate: The limit of vector sequence in a Hilbert space is , i.e. converges to . This means that for any real , no matter how small, there always exists an integer such that the norm of any later vector in the sequence minus the limit is less than . Definition of converge in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlimseqi 28046 | A sequence with a limit on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
Theorem | hlimveci 28047 | Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
Theorem | hlimconvi 28048* | Convergence of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlim2 28049* | The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlimadd 28050* | Limit of the sum of two sequences in a Hilbert vector space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
Theorem | hilmet 28051 | The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
Theorem | hilxmet 28052 | The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
Theorem | hilmetdval 28053 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
Theorem | hilims 28054 | Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.) |
Theorem | hhcau 28055 | The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
Theorem | hhlm 28056 | The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
Theorem | hhcmpl 28057* | Lemma used for derivation of the completeness axiom ax-hcompl 28059 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
Theorem | hilcompl 28058* | Lemma used for derivation of the completeness axiom ax-hcompl 28059 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 27856; the 6th would be satisfied by eqid 2622; the 7th by a given fixed Hilbert space; and the last by theorem hlcompl 27771. (Contributed by NM, 13-Sep-2007.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Axiom | ax-hcompl 28059* | Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
Theorem | hhcms 28060 | The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hhhl 28061 | The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hilcms 28062 | The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
Theorem | hilhl 28063 | The Hilbert space of the Hilbert Space Explorer is a complex Hilbert space. (Contributed by Steve Rodriguez, 29-Apr-2007.) (New usage is discouraged.) |
Definition | df-sh 28064 | Define the set of subspaces of a Hilbert space. See issh 28065 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | issh 28065 | Subspace of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | issh2 28066* | Subspace of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | shss 28067 | A subspace is a subset of Hilbert space. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | shel 28068 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
Theorem | shex 28069 | The set of subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
Theorem | shssii 28070 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Theorem | sheli 28071 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Theorem | shelii 28072 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Theorem | sh0 28073 | The zero vector belongs to any subspace of a Hilbert space. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | shaddcl 28074 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
Theorem | shmulcl 28075 | Closure of vector scalar multiplication in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
Theorem | issh3 28076* | Subspace of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
Theorem | shsubcl 28077 | Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
Definition | df-ch 28078 | Define the set of closed subspaces of a Hilbert space. A closed subspace is one in which the limit of every convergent sequence in the subspace belongs to the subspace. For its membership relation, see isch 28079. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 28080 and isch3 28098. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
Theorem | isch 28079 | Closed subspace of a Hilbert space. (Contributed by NM, 17-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | isch2 28080* | Closed subspace of a Hilbert space. Definition of [Beran] p. 107. (Contributed by NM, 17-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | chsh 28081 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | chsssh 28082 | Closed subspaces are subspaces in a Hilbert space. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | chex 28083 | The set of closed subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
Theorem | chshii 28084 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
Theorem | ch0 28085 | The zero vector belongs to any closed subspace of a Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.) |
Theorem | chss 28086 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.) |
Theorem | chel 28087 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
Theorem | chssii 28088 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Theorem | cheli 28089 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Theorem | chelii 28090 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
Theorem | chlimi 28091 | The limit property of a closed subspace of a Hilbert space. (Contributed by NM, 14-Sep-1999.) (New usage is discouraged.) |
Theorem | hlim0 28092 | The zero sequence in Hilbert space converges to the zero vector. (Contributed by NM, 17-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlimcaui 28093 | If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. (Contributed by NM, 17-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlimf 28094 | Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlimuni 28095 | A Hilbert space sequence converges to at most one limit. (Contributed by NM, 19-Aug-1999.) (Revised by Mario Carneiro, 2-May-2015.) (New usage is discouraged.) |
Theorem | hlimreui 28096* | The limit of a Hilbert space sequence is unique. (Contributed by NM, 19-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | hlimeui 28097* | The limit of a Hilbert space sequence is unique. (Contributed by NM, 19-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | isch3 28098* | A Hilbert subspace is closed iff it is complete. 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). Remark 3.12 of [Beran] p. 107. (Contributed by NM, 24-Dec-2001.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | chcompl 28099* | Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.) |
Theorem | helch 28100 | The unit Hilbert lattice element (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 6-Sep-1999.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |