![]() |
Metamath
Proof Explorer Theorem List (p. 305 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | norm3adifii 30401 | 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.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ (absβ((normββ(π΄ ββ πΆ)) β (normββ(π΅ ββ πΆ)))) β€ (normββ(π΄ ββ π΅)) | ||
Theorem | norm3lem 30402 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ (((normββ(π΄ ββ πΆ)) < (π· / 2) β§ (normββ(πΆ ββ π΅)) < (π· / 2)) β (normββ(π΄ ββ π΅)) < π·) | ||
Theorem | norm3dif 30403 | 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.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (normββ(π΄ ββ π΅)) β€ ((normββ(π΄ ββ πΆ)) + (normββ(πΆ ββ π΅)))) | ||
Theorem | norm3dif2 30404 | Norm of differences around common element. (Contributed by NM, 18-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (normββ(π΄ ββ π΅)) β€ ((normββ(πΆ ββ π΄)) + (normββ(πΆ ββ π΅)))) | ||
Theorem | norm3lemt 30405 | Lemma involving norm of differences in Hilbert space. (Contributed by NM, 18-Aug-1999.) (New usage is discouraged.) |
β’ (((π΄ β β β§ π΅ β β) β§ (πΆ β β β§ π· β β)) β (((normββ(π΄ ββ πΆ)) < (π· / 2) β§ (normββ(πΆ ββ π΅)) < (π· / 2)) β (normββ(π΄ ββ π΅)) < π·)) | ||
Theorem | norm3adifi 30406 | 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.) |
β’ πΆ β β β β’ ((π΄ β β β§ π΅ β β) β (absβ((normββ(π΄ ββ πΆ)) β (normββ(π΅ ββ πΆ)))) β€ (normββ(π΄ ββ π΅))) | ||
Theorem | normpari 30407 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 21-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (((normββ(π΄ ββ π΅))β2) + ((normββ(π΄ +β π΅))β2)) = ((2 Β· ((normββπ΄)β2)) + (2 Β· ((normββπ΅)β2))) | ||
Theorem | normpar 30408 | Parallelogram law for norms. Remark 3.4(B) of [Beran] p. 98. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (((normββ(π΄ ββ π΅))β2) + ((normββ(π΄ +β π΅))β2)) = ((2 Β· ((normββπ΄)β2)) + (2 Β· ((normββπ΅)β2)))) | ||
Theorem | normpar2i 30409 | 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.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β β β’ ((normββ(π΄ ββ π΅))β2) = (((2 Β· ((normββ(π΄ ββ πΆ))β2)) + (2 Β· ((normββ(π΅ ββ πΆ))β2))) β ((normββ((π΄ +β π΅) ββ (2 Β·β πΆ)))β2)) | ||
Theorem | polid2i 30410 | Generalized polarization identity. Generalization of Exercise 4(a) of [ReedSimon] p. 63. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β & β’ πΆ β β & β’ π· β β β β’ (π΄ Β·ih π΅) = (((((π΄ +β πΆ) Β·ih (π· +β π΅)) β ((π΄ ββ πΆ) Β·ih (π· ββ π΅))) + (i Β· (((π΄ +β (i Β·β πΆ)) Β·ih (π· +β (i Β·β π΅))) β ((π΄ ββ (i Β·β πΆ)) Β·ih (π· ββ (i Β·β π΅)))))) / 4) | ||
Theorem | polidi 30411 | 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 30337. (Contributed by NM, 30-Jun-2005.) (New usage is discouraged.) |
β’ π΄ β β & β’ π΅ β β β β’ (π΄ Β·ih π΅) = (((((normββ(π΄ +β π΅))β2) β ((normββ(π΄ ββ π΅))β2)) + (i Β· (((normββ(π΄ +β (i Β·β π΅)))β2) β ((normββ(π΄ ββ (i Β·β π΅)))β2)))) / 4) | ||
Theorem | polid 30412 | 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 30337. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ Β·ih π΅) = (((((normββ(π΄ +β π΅))β2) β ((normββ(π΄ ββ π΅))β2)) + (i Β· (((normββ(π΄ +β (i Β·β π΅)))β2) β ((normββ(π΄ ββ (i Β·β π΅)))β2)))) / 4)) | ||
Theorem | hilablo 30413 | Hilbert space vector addition is an Abelian group operation. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
β’ +β β AbelOp | ||
Theorem | hilid 30414 | The group identity element of Hilbert space vector addition is the zero vector. (Contributed by NM, 16-Apr-2007.) (New usage is discouraged.) |
β’ (GIdβ +β ) = 0β | ||
Theorem | hilvc 30415 | Hilbert space is a complex vector space. Vector addition is +β, and scalar product is Β·β. (Contributed by NM, 15-Apr-2007.) (New usage is discouraged.) |
β’ β¨ +β , Β·β β© β CVecOLD | ||
Theorem | hilnormi 30416 | 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.) |
β’ β = (BaseSetβπ) & β’ Β·ih = (Β·πOLDβπ) & β’ π β NrmCVec β β’ normβ = (normCVβπ) | ||
Theorem | hilhhi 30417 | Deduce the structure of Hilbert space from its components. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ β = (BaseSetβπ) & β’ +β = ( +π£ βπ) & β’ Β·β = ( Β·π OLD βπ) & β’ Β·ih = (Β·πOLDβπ) & β’ π β NrmCVec β β’ π = β¨β¨ +β , Β·β β©, normββ© | ||
Theorem | hhnv 30418 | Hilbert space is a normed complex vector space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ π β NrmCVec | ||
Theorem | hhva 30419 | The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ +β = ( +π£ βπ) | ||
Theorem | hhba 30420 | The base set of Hilbert space. This theorem provides an independent proof of df-hba 30222 (see comments in that definition). (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ β = (BaseSetβπ) | ||
Theorem | hh0v 30421 | The zero vector of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ 0β = (0vecβπ) | ||
Theorem | hhsm 30422 | The scalar product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ Β·β = ( Β·π OLD βπ) | ||
Theorem | hhvs 30423 | The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ ββ = ( βπ£ βπ) | ||
Theorem | hhnm 30424 | The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ normβ = (normCVβπ) | ||
Theorem | hhims 30425 | The induced metric of Hilbert space. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (normβ β ββ ) β β’ π· = (IndMetβπ) | ||
Theorem | hhims2 30426 | Hilbert space distance metric. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ π· = (normβ β ββ ) | ||
Theorem | hhmet 30427 | The induced metric of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ π· β (Metβ β) | ||
Theorem | hhxmet 30428 | The induced metric of Hilbert space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ π· β (βMetβ β) | ||
Theorem | hhmetdval 30429 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ ((π΄ β β β§ π΅ β β) β (π΄π·π΅) = (normββ(π΄ ββ π΅))) | ||
Theorem | hhip 30430 | The inner product operation of Hilbert space. (Contributed by NM, 17-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ Β·ih = (Β·πOLDβπ) | ||
Theorem | hhph 30431 | The Hilbert space of the Hilbert Space Explorer is an inner product space. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ π β CPreHilOLD | ||
Theorem | bcsiALT 30432 | 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.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ(π΄ Β·ih π΅)) β€ ((normββπ΄) Β· (normββπ΅)) | ||
Theorem | bcsiHIL 30433 | 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.) |
β’ π΄ β β & β’ π΅ β β β β’ (absβ(π΄ Β·ih π΅)) β€ ((normββπ΄) Β· (normββπ΅)) | ||
Theorem | bcs 30434 | Bunjakovaskij-Cauchy-Schwarz inequality. Remark 3.4 of [Beran] p. 98. (Contributed by NM, 16-Feb-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (absβ(π΄ Β·ih π΅)) β€ ((normββπ΄) Β· (normββπ΅))) | ||
Theorem | bcs2 30435 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 30433. (Contributed by NM, 24-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ (normββπ΄) β€ 1) β (absβ(π΄ Β·ih π΅)) β€ (normββπ΅)) | ||
Theorem | bcs3 30436 | Corollary of the Bunjakovaskij-Cauchy-Schwarz inequality bcsiHIL 30433. (Contributed by NM, 26-May-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β β§ (normββπ΅) β€ 1) β (absβ(π΄ Β·ih π΅)) β€ (normββπ΄)) | ||
Theorem | hcau 30437* | 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.) |
β’ (πΉ β Cauchy β (πΉ:ββΆ β β§ βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ¦) ββ (πΉβπ§))) < π₯)) | ||
Theorem | hcauseq 30438 | 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.) |
β’ (πΉ β Cauchy β πΉ:ββΆ β) | ||
Theorem | hcaucvg 30439* | 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.) |
β’ ((πΉ β Cauchy β§ π΄ β β+) β βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ¦) ββ (πΉβπ§))) < π΄) | ||
Theorem | seq1hcau 30440* | 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.) |
β’ (πΉ:ββΆ β β (πΉ β Cauchy β βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ¦) ββ (πΉβπ§))) < π₯)) | ||
Theorem | hlimi 30441* | 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.) |
β’ π΄ β V β β’ (πΉ βπ£ π΄ β ((πΉ:ββΆ β β§ π΄ β β) β§ βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ§) ββ π΄)) < π₯)) | ||
Theorem | hlimseqi 30442 | A sequence with a limit on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β V β β’ (πΉ βπ£ π΄ β πΉ:ββΆ β) | ||
Theorem | hlimveci 30443 | Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β V β β’ (πΉ βπ£ π΄ β π΄ β β) | ||
Theorem | hlimconvi 30444* | 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.) |
β’ π΄ β V β β’ ((πΉ βπ£ π΄ β§ π΅ β β+) β βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ§) ββ π΄)) < π΅) | ||
Theorem | hlim2 30445* | 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.) |
β’ ((πΉ:ββΆ β β§ π΄ β β) β (πΉ βπ£ π΄ β βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ§) ββ π΄)) < π₯)) | ||
Theorem | hlimadd 30446* | 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 30447 | The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ π· β (Metβ β) | ||
Theorem | hilxmet 30448 | The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ π· β (βMetβ β) | ||
Theorem | hilmetdval 30449 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ ((π΄ β β β§ π΅ β β) β (π΄π·π΅) = (normββ(π΄ ββ π΅))) | ||
Theorem | hilims 30450 | Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.) |
β’ β = (BaseSetβπ) & β’ +β = ( +π£ βπ) & β’ Β·β = ( Β·π OLD βπ) & β’ Β·ih = (Β·πOLDβπ) & β’ π· = (IndMetβπ) & β’ π β NrmCVec β β’ π· = (normβ β ββ ) | ||
Theorem | hhcau 30451 | The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ Cauchy = ((Cauβπ·) β© ( β βm β)) | ||
Theorem | hhlm 30452 | The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) β β’ βπ£ = ((βπ‘βπ½) βΎ ( β βm β)) | ||
Theorem | hhcmpl 30453* | Lemma used for derivation of the completeness axiom ax-hcompl 30455 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ (πΉ β (Cauβπ·) β βπ₯ β β πΉ(βπ‘βπ½)π₯) β β’ (πΉ β Cauchy β βπ₯ β β πΉ βπ£ π₯) | ||
Theorem | hilcompl 30454* | Lemma used for derivation of the completeness axiom ax-hcompl 30455 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 30252; the 6th would be satisfied by eqid 2733; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl 30168. (Contributed by NM, 13-Sep-2007.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ β = (BaseSetβπ) & β’ +β = ( +π£ βπ) & β’ Β·β = ( Β·π OLD βπ) & β’ Β·ih = (Β·πOLDβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CHilOLD & β’ (πΉ β (Cauβπ·) β βπ₯ β β πΉ(βπ‘βπ½)π₯) β β’ (πΉ β Cauchy β βπ₯ β β πΉ βπ£ π₯) | ||
Axiom | ax-hcompl 30455* | Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
β’ (πΉ β Cauchy β βπ₯ β β πΉ βπ£ π₯) | ||
Theorem | hhcms 30456 | The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008.) (Proof shortened by Mario Carneiro, 14-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ π· β (CMetβ β) | ||
Theorem | hhhl 30457 | The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ π β CHilOLD | ||
Theorem | hilcms 30458 | The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ π· β (CMetβ β) | ||
Theorem | hilhl 30459 | The Hilbert space of the Hilbert Space Explorer is a complex Hilbert space. (Contributed by Steve Rodriguez, 29-Apr-2007.) (New usage is discouraged.) |
β’ β¨β¨ +β , Β·β β©, normββ© β CHilOLD | ||
Definition | df-sh 30460 | Define the set of subspaces of a Hilbert space. See issh 30461 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.) |
β’ Sβ = {β β π« β β£ (0β β β β§ ( +β β (β Γ β)) β β β§ ( Β·β β (β Γ β)) β β)} | ||
Theorem | issh 30461 | 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.) |
β’ (π» β Sβ β ((π» β β β§ 0β β π») β§ (( +β β (π» Γ π»)) β π» β§ ( Β·β β (β Γ π»)) β π»))) | ||
Theorem | issh2 30462* | 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.) |
β’ (π» β Sβ β ((π» β β β§ 0β β π») β§ (βπ₯ β π» βπ¦ β π» (π₯ +β π¦) β π» β§ βπ₯ β β βπ¦ β π» (π₯ Β·β π¦) β π»))) | ||
Theorem | shss 30463 | 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.) |
β’ (π» β Sβ β π» β β) | ||
Theorem | shel 30464 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β π») β π΄ β β) | ||
Theorem | shex 30465 | The set of subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ Sβ β V | ||
Theorem | shssii 30466 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Sβ β β’ π» β β | ||
Theorem | sheli 30467 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Sβ β β’ (π΄ β π» β π΄ β β) | ||
Theorem | shelii 30468 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Sβ & β’ π΄ β π» β β’ π΄ β β | ||
Theorem | sh0 30469 | 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.) |
β’ (π» β Sβ β 0β β π») | ||
Theorem | shaddcl 30470 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β π» β§ π΅ β π») β (π΄ +β π΅) β π») | ||
Theorem | shmulcl 30471 | Closure of vector scalar multiplication in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β β β§ π΅ β π») β (π΄ Β·β π΅) β π») | ||
Theorem | issh3 30472* | Subspace π» of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ (π» β β β (π» β Sβ β (0β β π» β§ (βπ₯ β π» βπ¦ β π» (π₯ +β π¦) β π» β§ βπ₯ β β βπ¦ β π» (π₯ Β·β π¦) β π»)))) | ||
Theorem | shsubcl 30473 | Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β π» β§ π΅ β π») β (π΄ ββ π΅) β π») | ||
Definition | df-ch 30474 | 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 30475. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 30476 and isch3 30494. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
β’ Cβ = {β β Sβ β£ ( βπ£ β (β βm β)) β β} | ||
Theorem | isch 30475 | Closed subspace π» of a Hilbert space. (Contributed by NM, 17-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Cβ β (π» β Sβ β§ ( βπ£ β (π» βm β)) β π»)) | ||
Theorem | isch2 30476* | 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.) |
β’ (π» β Cβ β (π» β Sβ β§ βπβπ₯((π:ββΆπ» β§ π βπ£ π₯) β π₯ β π»))) | ||
Theorem | chsh 30477 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Cβ β π» β Sβ ) | ||
Theorem | chsssh 30478 | 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.) |
β’ Cβ β Sβ | ||
Theorem | chex 30479 | The set of closed subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ Cβ β V | ||
Theorem | chshii 30480 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ π» β Sβ | ||
Theorem | ch0 30481 | The zero vector belongs to any closed subspace of a Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.) |
β’ (π» β Cβ β 0β β π») | ||
Theorem | chss 30482 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.) |
β’ (π» β Cβ β π» β β) | ||
Theorem | chel 30483 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β π») β π΄ β β) | ||
Theorem | chssii 30484 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ π» β β | ||
Theorem | cheli 30485 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (π΄ β π» β π΄ β β) | ||
Theorem | chelii 30486 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β π» β β’ π΄ β β | ||
Theorem | chlimi 30487 | The limit property of a closed subspace of a Hilbert space. (Contributed by NM, 14-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β V β β’ ((π» β Cβ β§ πΉ:ββΆπ» β§ πΉ βπ£ π΄) β π΄ β π») | ||
Theorem | hlim0 30488 | 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.) |
β’ (β Γ {0β}) βπ£ 0β | ||
Theorem | hlimcaui 30489 | 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.) |
β’ (πΉ βπ£ π΄ β πΉ β Cauchy) | ||
Theorem | hlimf 30490 | Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ βπ£ :dom βπ£ βΆ β | ||
Theorem | hlimuni 30491 | 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 30492* | 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 30493* | 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 30494* | 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.) |
β’ (π» β Cβ β (π» β Sβ β§ βπ β Cauchy (π:ββΆπ» β βπ₯ β π» π βπ£ π₯))) | ||
Theorem | chcompl 30495* | Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ πΉ β Cauchy β§ πΉ:ββΆπ») β βπ₯ β π» πΉ βπ£ π₯) | ||
Theorem | helch 30496 | The Hilbert lattice one (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.) |
β’ β β Cβ | ||
Theorem | ifchhv 30497 | Prove if(π΄ β Cβ , π΄, β) β Cβ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.) |
β’ if(π΄ β Cβ , π΄, β) β Cβ | ||
Theorem | helsh 30498 | Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
β’ β β Sβ | ||
Theorem | shsspwh 30499 | Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
β’ Sβ β π« β | ||
Theorem | chsspwh 30500 | Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
β’ Cβ β π« β |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |