![]() |
Metamath
Proof Explorer Theorem List (p. 304 of 480) | < 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-30438) |
![]() (30439-31961) |
![]() (31962-47939) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bloval 30301* | The class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π΅ = {π‘ β πΏ β£ (πβπ‘) < +β}) | ||
Theorem | isblo 30302 | The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β (π β π΅ β (π β πΏ β§ (πβπ) < +β))) | ||
Theorem | isblo2 30303 | The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β (π β π΅ β (π β πΏ β§ (πβπ) β β))) | ||
Theorem | bloln 30304 | A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π β πΏ) | ||
Theorem | blof 30305 | A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π:πβΆπ) | ||
Theorem | nmblore 30306 | The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (π normOpOLD π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β (πβπ) β β) | ||
Theorem | 0ofval 30307 | The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π = (π Γ {π})) | ||
Theorem | 0oval 30308 | Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π΄ β π) β (πβπ΄) = π) | ||
Theorem | 0oo 30309 | The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π:πβΆπ) | ||
Theorem | 0lno 30310 | The zero operator is linear. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
β’ π = (π 0op π) & β’ πΏ = (π LnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π β πΏ) | ||
Theorem | nmoo0 30311 | The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec) β (πβπ) = 0) | ||
Theorem | 0blo 30312 | The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (π 0op π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π β π΅) | ||
Theorem | nmlno0lem 30313 | Lemma for nmlno0i 30314. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ π = (π 0op π) & β’ πΏ = (π LnOp π) & β’ π β NrmCVec & β’ π β NrmCVec & β’ π β πΏ & β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (0vecβπ) & β’ π = (0vecβπ) & β’ πΎ = (normCVβπ) & β’ π = (normCVβπ) β β’ ((πβπ) = 0 β π = π) | ||
Theorem | nmlno0i 30314 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ π = (π 0op π) & β’ πΏ = (π LnOp π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ (π β πΏ β ((πβπ) = 0 β π = π)) | ||
Theorem | nmlno0 30315 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ π = (π 0op π) & β’ πΏ = (π LnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β ((πβπ) = 0 β π = π)) | ||
Theorem | nmlnoubi 30316* | An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ πΎ = (normCVβπ) & β’ π = (normCVβπ) & β’ π = (π normOpOLD π) & β’ πΏ = (π LnOp π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ ((π β πΏ β§ (π΄ β β β§ 0 β€ π΄) β§ βπ₯ β π (π₯ β π β (πβ(πβπ₯)) β€ (π΄ Β· (πΎβπ₯)))) β (πβπ) β€ π΄) | ||
Theorem | nmlnogt0 30317 | The norm of a nonzero linear operator is positive. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ π = (π 0op π) & β’ πΏ = (π LnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β (π β π β 0 < (πβπ))) | ||
Theorem | lnon0 30318* | The domain of a nonzero linear operator contains a nonzero vector. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (π 0op π) & β’ πΏ = (π LnOp π) β β’ (((π β NrmCVec β§ π β NrmCVec β§ π β πΏ) β§ π β π) β βπ₯ β π π₯ β π) | ||
Theorem | nmblolbii 30319 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΏ = (normCVβπ) & β’ π = (normCVβπ) & β’ π = (π normOpOLD π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec & β’ π β π΅ β β’ (π΄ β π β (πβ(πβπ΄)) β€ ((πβπ) Β· (πΏβπ΄))) | ||
Theorem | nmblolbi 30320 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΏ = (normCVβπ) & β’ π = (normCVβπ) & β’ π = (π normOpOLD π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ ((π β π΅ β§ π΄ β π) β (πβ(πβπ΄)) β€ ((πβπ) Β· (πΏβπ΄))) | ||
Theorem | isblo3i 30321* | The predicate "is a bounded linear operator." Definition 2.7-1 of [Kreyszig] p. 91. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (normCVβπ) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ (π β π΅ β (π β πΏ β§ βπ₯ β β βπ¦ β π (πβ(πβπ¦)) β€ (π₯ Β· (πβπ¦)))) | ||
Theorem | blo3i 30322* | Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (normCVβπ) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ ((π β πΏ β§ π΄ β β β§ βπ¦ β π (πβ(πβπ¦)) β€ (π΄ Β· (πβπ¦))) β π β π΅) | ||
Theorem | blometi 30323 | Upper bound for the distance between the values of a bounded linear operator. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ πΆ = (IndMetβπ) & β’ π· = (IndMetβπ) & β’ π = (π normOpOLD π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ ((π β π΅ β§ π β π β§ π β π) β ((πβπ)π·(πβπ)) β€ ((πβπ) Β· (ππΆπ))) | ||
Theorem | blocnilem 30324 | Lemma for blocni 30325 and lnocni 30326. If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec & β’ π β πΏ & β’ π = (BaseSetβπ) β β’ ((π β π β§ π β ((π½ CnP πΎ)βπ)) β π β π΅) | ||
Theorem | blocni 30325 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec & β’ π β πΏ β β’ (π β (π½ Cn πΎ) β π β π΅) | ||
Theorem | lnocni 30326 | If a linear operator is continuous at any point, it is continuous everywhere. Theorem 2.7-9(b) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec & β’ π β πΏ & β’ π = (BaseSetβπ) β β’ ((π β π β§ π β ((π½ CnP πΎ)βπ)) β π β (π½ Cn πΎ)) | ||
Theorem | blocn 30327 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec & β’ πΏ = (π LnOp π) β β’ (π β πΏ β (π β (π½ Cn πΎ) β π β π΅)) | ||
Theorem | blocn2 30328 | A bounded linear operator is continuous. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ π΅ = (π BLnOp π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ (π β π΅ β π β (π½ Cn πΎ)) | ||
Theorem | ajfval 30329* | The adjoint function. (Contributed by NM, 25-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π = (Β·πOLDβπ) & β’ π΄ = (πadjπ) β β’ ((π β NrmCVec β§ π β NrmCVec) β π΄ = {β¨π‘, π β© β£ (π‘:πβΆπ β§ π :πβΆπ β§ βπ₯ β π βπ¦ β π ((π‘βπ₯)ππ¦) = (π₯π(π βπ¦)))}) | ||
Theorem | hmoval 30330* | The set of Hermitian (self-adjoint) operators on a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π» = (HmOpβπ) & β’ π΄ = (πadjπ) β β’ (π β NrmCVec β π» = {π‘ β dom π΄ β£ (π΄βπ‘) = π‘}) | ||
Theorem | ishmo 30331 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π» = (HmOpβπ) & β’ π΄ = (πadjπ) β β’ (π β NrmCVec β (π β π» β (π β dom π΄ β§ (π΄βπ) = π))) | ||
Syntax | ccphlo 30332 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
class CPreHilOLD | ||
Definition | df-ph 30333* | Define the class of all complex inner product spaces. An inner product space is a normed vector space whose norm satisfies the parallelogram law (a property that induces an inner product). Based on Exercise 4(b) of [ReedSimon] p. 63. The vector operation is π, the scalar product is π , and the norm is π. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
β’ CPreHilOLD = (NrmCVec β© {β¨β¨π, π β©, πβ© β£ βπ₯ β ran πβπ¦ β ran π(((πβ(π₯ππ¦))β2) + ((πβ(π₯π(-1π π¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))}) | ||
Theorem | phnv 30334 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
β’ (π β CPreHilOLD β π β NrmCVec) | ||
Theorem | phrel 30335 | The class of all complex inner product spaces is a relation. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
β’ Rel CPreHilOLD | ||
Theorem | phnvi 30336 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π β CPreHilOLD β β’ π β NrmCVec | ||
Theorem | isphg 30337* | The predicate "is a complex inner product space." An inner product space is a normed vector space whose norm satisfies the parallelogram law. The vector (group) addition operation is πΊ, the scalar product is π, and the norm is π. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
β’ π = ran πΊ β β’ ((πΊ β π΄ β§ π β π΅ β§ π β πΆ) β (β¨β¨πΊ, πβ©, πβ© β CPreHilOLD β (β¨β¨πΊ, πβ©, πβ© β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯πΊ(-1ππ¦)))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2)))))) | ||
Theorem | phop 30338 | A complex inner product space in terms of ordered pair components. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) β β’ (π β CPreHilOLD β π = β¨β¨πΊ, πβ©, πβ©) | ||
Theorem | cncph 30339 | The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 7-Nov-2013.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ π β CPreHilOLD | ||
Theorem | elimph 30340 | Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π β CPreHilOLD β β’ if(π΄ β π, π΄, π) β π | ||
Theorem | elimphu 30341 | Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 6-May-2007.) (New usage is discouraged.) |
β’ if(π β CPreHilOLD, π, β¨β¨ + , Β· β©, absβ©) β CPreHilOLD | ||
Theorem | isph 30342* | The predicate "is an inner product space." (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) β β’ (π β CPreHilOLD β (π β NrmCVec β§ βπ₯ β π βπ¦ β π (((πβ(π₯πΊπ¦))β2) + ((πβ(π₯ππ¦))β2)) = (2 Β· (((πβπ₯)β2) + ((πβπ¦)β2))))) | ||
Theorem | phpar2 30343 | The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) β β’ ((π β CPreHilOLD β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄ππ΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | phpar 30344 | The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) β β’ ((π β CPreHilOLD β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | ip0i 30345 | A slight variant of Equation 6.46 of [Ponnusamy] p. 362, where π½ is either 1 or -1 to represent +-1. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π = (normCVβπ) & β’ π½ β β β β’ ((((πβ((π΄πΊπ΅)πΊ(π½ππΆ)))β2) β ((πβ((π΄πΊπ΅)πΊ(-π½ππΆ)))β2)) + (((πβ((π΄πΊ(-1ππ΅))πΊ(π½ππΆ)))β2) β ((πβ((π΄πΊ(-1ππ΅))πΊ(-π½ππΆ)))β2))) = (2 Β· (((πβ(π΄πΊ(π½ππΆ)))β2) β ((πβ(π΄πΊ(-π½ππΆ)))β2))) | ||
Theorem | ip1ilem 30346 | Lemma for ip1i 30347. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π = (normCVβπ) & β’ π½ β β β β’ (((π΄πΊπ΅)ππΆ) + ((π΄πΊ(-1ππ΅))ππΆ)) = (2 Β· (π΄ππΆ)) | ||
Theorem | ip1i 30347 | Equation 6.47 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π β β’ (((π΄πΊπ΅)ππΆ) + ((π΄πΊ(-1ππ΅))ππΆ)) = (2 Β· (π΄ππΆ)) | ||
Theorem | ip2i 30348 | Equation 6.48 of [Ponnusamy] p. 362. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ ((2ππ΄)ππ΅) = (2 Β· (π΄ππ΅)) | ||
Theorem | ipdirilem 30349 | Lemma for ipdiri 30350. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π β β’ ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ)) | ||
Theorem | ipdiri 30350 | Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π΄ β π β§ π΅ β π β§ πΆ β π) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ))) | ||
Theorem | ipasslem1 30351 | Lemma for ipassi 30361. Show the inner product associative law for nonnegative integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΅ β π β β’ ((π β β0 β§ π΄ β π) β ((πππ΄)ππ΅) = (π Β· (π΄ππ΅))) | ||
Theorem | ipasslem2 30352 | Lemma for ipassi 30361. Show the inner product associative law for nonpositive integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΅ β π β β’ ((π β β0 β§ π΄ β π) β ((-πππ΄)ππ΅) = (-π Β· (π΄ππ΅))) | ||
Theorem | ipasslem3 30353 | Lemma for ipassi 30361. Show the inner product associative law for all integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΅ β π β β’ ((π β β€ β§ π΄ β π) β ((πππ΄)ππ΅) = (π Β· (π΄ππ΅))) | ||
Theorem | ipasslem4 30354 | Lemma for ipassi 30361. Show the inner product associative law for positive integer reciprocals. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΅ β π β β’ ((π β β β§ π΄ β π) β (((1 / π)ππ΄)ππ΅) = ((1 / π) Β· (π΄ππ΅))) | ||
Theorem | ipasslem5 30355 | Lemma for ipassi 30361. Show the inner product associative law for rational numbers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΅ β π β β’ ((πΆ β β β§ π΄ β π) β ((πΆππ΄)ππ΅) = (πΆ Β· (π΄ππ΅))) | ||
Theorem | ipasslem7 30356* | Lemma for ipassi 30361. Show that ((π€ππ΄)ππ΅) β (π€ Β· (π΄ππ΅)) is continuous on β. (Contributed by NM, 23-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΉ = (π€ β β β¦ (((π€ππ΄)ππ΅) β (π€ Β· (π΄ππ΅)))) & β’ π½ = (topGenβran (,)) & β’ πΎ = (TopOpenββfld) β β’ πΉ β (π½ Cn πΎ) | ||
Theorem | ipasslem8 30357* | Lemma for ipassi 30361. By ipasslem5 30355, πΉ is 0 for all β; since it is continuous and β is dense in β by qdensere2 24533, we conclude πΉ is 0 for all β. (Contributed by NM, 24-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΉ = (π€ β β β¦ (((π€ππ΄)ππ΅) β (π€ Β· (π΄ππ΅)))) β β’ πΉ:ββΆ{0} | ||
Theorem | ipasslem9 30358 | Lemma for ipassi 30361. Conclude from ipasslem8 30357 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (πΆ β β β ((πΆππ΄)ππ΅) = (πΆ Β· (π΄ππ΅))) | ||
Theorem | ipasslem10 30359 | Lemma for ipassi 30361. Show the inner product associative law for the imaginary number i. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = (normCVβπ) β β’ ((iππ΄)ππ΅) = (i Β· (π΄ππ΅)) | ||
Theorem | ipasslem11 30360 | Lemma for ipassi 30361. Show the inner product associative law for all complex numbers. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (πΆ β β β ((πΆππ΄)ππ΅) = (πΆ Β· (π΄ππ΅))) | ||
Theorem | ipassi 30361 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π΄ β β β§ π΅ β π β§ πΆ β π) β ((π΄ππ΅)ππΆ) = (π΄ Β· (π΅ππΆ))) | ||
Theorem | dipdir 30362 | Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ))) | ||
Theorem | dipdi 30363 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅) + (π΄ππΆ))) | ||
Theorem | ip2dii 30364 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π· β π β β’ ((π΄πΊπ΅)π(πΆπΊπ·)) = (((π΄ππΆ) + (π΅ππ·)) + ((π΄ππ·) + (π΅ππΆ))) | ||
Theorem | dipass 30365 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = (π΄ Β· (π΅ππΆ))) | ||
Theorem | dipassr 30366 | "Associative" law for second argument of inner product (compare dipass 30365). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((ββπ΅) Β· (π΄ππΆ))) | ||
Theorem | dipassr2 30367 | "Associative" law for inner product. Conjugate version of dipassr 30366. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π((ββπ΅)ππΆ)) = (π΅ Β· (π΄ππΆ))) | ||
Theorem | dipsubdir 30368 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = ((π΄ππΆ) β (π΅ππΆ))) | ||
Theorem | dipsubdi 30369 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((π΄ππ΅) β (π΄ππΆ))) | ||
Theorem | pythi 30370 | The Pythagorean theorem for an arbitrary complex inner product (pre-Hilbert) space π. The square of the norm of the sum of two orthogonal vectors (i.e. whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ ((π΄ππ΅) = 0 β ((πβ(π΄πΊπ΅))β2) = (((πβπ΄)β2) + ((πβπ΅)β2))) | ||
Theorem | siilem1 30371 | Lemma for sii 30374. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) & β’ πΆ β β & β’ (πΆ Β· (π΄ππ΅)) β β & β’ 0 β€ (πΆ Β· (π΄ππ΅)) β β’ ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | siilem2 30372 | Lemma for sii 30374. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((πΆ β β β§ (πΆ Β· (π΄ππ΅)) β β β§ 0 β€ (πΆ Β· (π΄ππ΅))) β ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅)))) | ||
Theorem | siii 30373 | Inference from sii 30374. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅)) | ||
Theorem | sii 30374 | Obsolete version of ipcau 24986 as of 22-Sep-2024. Schwarz inequality. Part of Lemma 3-2.1(a) of [Kreyszig] p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also Theorems bcseqi 30640, bcsiALT 30699, bcsiHIL 30700, csbren 25147. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π΄ β π β§ π΅ β π) β (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | ipblnfi 30375* | A function πΉ generated by varying the first argument of an inner product (with its second argument a fixed vector π΄) is a bounded linear functional, i.e. a bounded linear operator from the vector space to β. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ πΆ = β¨β¨ + , Β· β©, absβ© & β’ π΅ = (π BLnOp πΆ) & β’ πΉ = (π₯ β π β¦ (π₯ππ΄)) β β’ (π΄ β π β πΉ β π΅) | ||
Theorem | ip2eqi 30376* | Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π΄ β π β§ π΅ β π) β (βπ₯ β π (π₯ππ΄) = (π₯ππ΅) β π΄ = π΅)) | ||
Theorem | phoeqi 30377* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π:πβΆπ β§ π:πβΆπ) β (βπ₯ β π βπ¦ β π (π₯π(πβπ¦)) = (π₯π(πβπ¦)) β π = π)) | ||
Theorem | ajmoi 30378* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ β*π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))) | ||
Theorem | ajfuni 30379 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) & β’ π β CPreHilOLD & β’ π β NrmCVec β β’ Fun π΄ | ||
Theorem | ajfun 30380 | The adjoint function is a function. This is not immediately apparent from df-aj 30270 but results from the uniqueness shown by ajmoi 30378. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec) β Fun π΄) | ||
Theorem | ajval 30381* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π = (Β·πOLDβπ) & β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec β§ π:πβΆπ) β (π΄βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) | ||
Syntax | ccbn 30382 | Extend class notation with the class of all complex Banach spaces. |
class CBan | ||
Definition | df-cbn 30383 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 25084 instead. (New usage is discouraged.) |
β’ CBan = {π’ β NrmCVec β£ (IndMetβπ’) β (CMetβ(BaseSetβπ’))} | ||
Theorem | iscbn 30384 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 25086 instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β (π β NrmCVec β§ π· β (CMetβπ))) | ||
Theorem | cbncms 30385 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 25095 (or preferably bncms 25092) instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β π· β (CMetβπ)) | ||
Theorem | bnnv 30386 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 25088 instead. (New usage is discouraged.) |
β’ (π β CBan β π β NrmCVec) | ||
Theorem | bnrel 30387 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CBan | ||
Theorem | bnsscmcl 30388 | A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π» = (SubSpβπ) & β’ π = (BaseSetβπ) β β’ ((π β CBan β§ π β π») β (π β CBan β π β (Clsdβπ½))) | ||
Theorem | cnbn 30389 | The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ π β CBan | ||
Theorem | ubthlem1 30390* | Lemma for ubth 30393. The function π΄ exhibits a countable collection of sets that are closed, being the inverse image under π‘ of the closed ball of radius π, and by assumption they cover π. Thus, by the Baire Category theorem bcth2 25078, for some π the set π΄βπ has an interior, meaning that there is a closed ball {π§ β π β£ (π¦π·π§) β€ π} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) & β’ (π β βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π) & β’ π΄ = (π β β β¦ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) β β’ (π β βπ β β βπ¦ β π βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)) | ||
Theorem | ubthlem2 30391* | Lemma for ubth 30393. Given that there is a closed ball π΅(π, π ) in π΄βπΎ, for any π₯ β π΅(0, 1), we have π + π Β· π₯ β π΅(π, π ) and π β π΅(π, π ), so both of these have norm(π‘(π§)) β€ πΎ and so norm(π‘(π₯ )) β€ (norm(π‘(π)) + norm(π‘(π + π Β· π₯))) / π β€ ( πΎ + πΎ) / π , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) & β’ (π β βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π) & β’ π΄ = (π β β β¦ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) & β’ (π β πΎ β β) & β’ (π β π β π) & β’ (π β π β β+) & β’ (π β {π§ β π β£ (ππ·π§) β€ π } β (π΄βπΎ)) β β’ (π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π) | ||
Theorem | ubthlem3 30392* | Lemma for ubth 30393. Prove the reverse implication, using nmblolbi 30320. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) β β’ (π β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π)) | ||
Theorem | ubth 30393* | Uniform Boundedness Theorem, also called the Banach-Steinhaus Theorem. Let π be a collection of bounded linear operators on a Banach space. If, for every vector π₯, the norms of the operators' values are bounded, then the operators' norms are also bounded. Theorem 4.7-3 of [Kreyszig] p. 249. See also http://en.wikipedia.org/wiki/Uniform_boundedness_principle. (Contributed by NM, 7-Nov-2007.) (Proof shortened by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (π normOpOLD π) β β’ ((π β CBan β§ π β NrmCVec β§ π β (π BLnOp π)) β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π (πβπ‘) β€ π)) | ||
Theorem | minvecolem1 30394* | Lemma for minveco 30404. The set of all distances from points of π to π΄ are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) β β’ (π β (π β β β§ π β β β§ βπ€ β π 0 β€ π€)) | ||
Theorem | minvecolem2 30395* | Lemma for minveco 30404. Any two points πΎ and πΏ in π are close to each other if they are close to the infimum of distance to π΄. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β ((π΄π·πΎ)β2) β€ ((πβ2) + π΅)) & β’ (π β ((π΄π·πΏ)β2) β€ ((πβ2) + π΅)) β β’ (π β ((πΎπ·πΏ)β2) β€ (4 Β· π΅)) | ||
Theorem | minvecolem3 30396* | Lemma for minveco 30404. The sequence formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β πΉ β (Cauβπ·)) | ||
Theorem | minvecolem4a 30397* | Lemma for minveco 30404. πΉ is convergent in the subspace topology on π. (Contributed by Mario Carneiro, 7-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) | ||
Theorem | minvecolem4b 30398* | Lemma for minveco 30404. The convergent point of the cauchy sequence πΉ is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β ((βπ‘βπ½)βπΉ) β π) | ||
Theorem | minvecolem4c 30399* | Lemma for minveco 30404. The infimum of the distances to π΄ is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β π β β) | ||
Theorem | minvecolem4 30400* | Lemma for minveco 30404. The convergent point of the cauchy sequence πΉ attains the minimum distance, and so is closer to π΄ than any other point in π. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) & β’ π = (1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |