![]() |
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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | bloln 30301 | A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π β πΏ) | ||
Theorem | blof 30302 | A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π:πβΆπ) | ||
Theorem | nmblore 30303 | 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 30304 | 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 30305 | Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π΄ β π) β (πβπ΄) = π) | ||
Theorem | 0oo 30306 | The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π:πβΆπ) | ||
Theorem | 0lno 30307 | 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 30308 | The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec) β (πβπ) = 0) | ||
Theorem | 0blo 30309 | The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (π 0op π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π β π΅) | ||
Theorem | nmlno0lem 30310 | Lemma for nmlno0i 30311. (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 30311 | 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 30312 | 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 30313* | 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 30314 | 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 30315* | 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 30316 | 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 30317 | 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 30318* | 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 30319* | 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 30320 | 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 30321 | Lemma for blocni 30322 and lnocni 30323. 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 30322 | 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 30323 | 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 30324 | 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 30325 | 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 30326* | 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 30327* | 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 30328 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π» = (HmOpβπ) & β’ π΄ = (πadjπ) β β’ (π β NrmCVec β (π β π» β (π β dom π΄ β§ (π΄βπ) = π))) | ||
Syntax | ccphlo 30329 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
class CPreHilOLD | ||
Definition | df-ph 30330* | 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 30331 | 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 30332 | 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 30333 | 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 30334* | 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 30335 | 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 30336 | 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 30337 | 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 30338 | 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 30339* | 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 30340 | 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 30341 | 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 30342 | 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 30343 | Lemma for ip1i 30344. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π = (normCVβπ) & β’ π½ β β β β’ (((π΄πΊπ΅)ππΆ) + ((π΄πΊ(-1ππ΅))ππΆ)) = (2 Β· (π΄ππΆ)) | ||
Theorem | ip1i 30344 | 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 30345 | 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 30346 | Lemma for ipdiri 30347. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π β β’ ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ)) | ||
Theorem | ipdiri 30347 | 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 30348 | Lemma for ipassi 30358. 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 30349 | Lemma for ipassi 30358. 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 30350 | Lemma for ipassi 30358. 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 30351 | Lemma for ipassi 30358. 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 30352 | Lemma for ipassi 30358. 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 30353* | Lemma for ipassi 30358. 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 30354* | Lemma for ipassi 30358. By ipasslem5 30352, πΉ is 0 for all β; since it is continuous and β is dense in β by qdensere2 24534, 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 30355 | Lemma for ipassi 30358. Conclude from ipasslem8 30354 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (πΆ β β β ((πΆππ΄)ππ΅) = (πΆ Β· (π΄ππ΅))) | ||
Theorem | ipasslem10 30356 | Lemma for ipassi 30358. 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 30357 | Lemma for ipassi 30358. 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 30358 | 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 30359 | 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 30360 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅) + (π΄ππΆ))) | ||
Theorem | ip2dii 30361 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π· β π β β’ ((π΄πΊπ΅)π(πΆπΊπ·)) = (((π΄ππΆ) + (π΅ππ·)) + ((π΄ππ·) + (π΅ππΆ))) | ||
Theorem | dipass 30362 | 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 30363 | "Associative" law for second argument of inner product (compare dipass 30362). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((ββπ΅) Β· (π΄ππΆ))) | ||
Theorem | dipassr2 30364 | "Associative" law for inner product. Conjugate version of dipassr 30363. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π((ββπ΅)ππΆ)) = (π΅ Β· (π΄ππΆ))) | ||
Theorem | dipsubdir 30365 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = ((π΄ππΆ) β (π΅ππΆ))) | ||
Theorem | dipsubdi 30366 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((π΄ππ΅) β (π΄ππΆ))) | ||
Theorem | pythi 30367 | 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 30368 | Lemma for sii 30371. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) & β’ πΆ β β & β’ (πΆ Β· (π΄ππ΅)) β β & β’ 0 β€ (πΆ Β· (π΄ππ΅)) β β’ ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | siilem2 30369 | Lemma for sii 30371. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((πΆ β β β§ (πΆ Β· (π΄ππ΅)) β β β§ 0 β€ (πΆ Β· (π΄ππ΅))) β ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅)))) | ||
Theorem | siii 30370 | Inference from sii 30371. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅)) | ||
Theorem | sii 30371 | Obsolete version of ipcau 24987 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 30637, bcsiALT 30696, bcsiHIL 30697, csbren 25148. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π΄ β π β§ π΅ β π) β (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | ipblnfi 30372* | 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 30373* | 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 30374* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π:πβΆπ β§ π:πβΆπ) β (βπ₯ β π βπ¦ β π (π₯π(πβπ¦)) = (π₯π(πβπ¦)) β π = π)) | ||
Theorem | ajmoi 30375* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ β*π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))) | ||
Theorem | ajfuni 30376 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) & β’ π β CPreHilOLD & β’ π β NrmCVec β β’ Fun π΄ | ||
Theorem | ajfun 30377 | The adjoint function is a function. This is not immediately apparent from df-aj 30267 but results from the uniqueness shown by ajmoi 30375. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec) β Fun π΄) | ||
Theorem | ajval 30378* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π = (Β·πOLDβπ) & β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec β§ π:πβΆπ) β (π΄βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) | ||
Syntax | ccbn 30379 | Extend class notation with the class of all complex Banach spaces. |
class CBan | ||
Definition | df-cbn 30380 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 25085 instead. (New usage is discouraged.) |
β’ CBan = {π’ β NrmCVec β£ (IndMetβπ’) β (CMetβ(BaseSetβπ’))} | ||
Theorem | iscbn 30381 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 25087 instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β (π β NrmCVec β§ π· β (CMetβπ))) | ||
Theorem | cbncms 30382 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 25096 (or preferably bncms 25093) instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β π· β (CMetβπ)) | ||
Theorem | bnnv 30383 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 25089 instead. (New usage is discouraged.) |
β’ (π β CBan β π β NrmCVec) | ||
Theorem | bnrel 30384 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CBan | ||
Theorem | bnsscmcl 30385 | 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 30386 | 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 30387* | Lemma for ubth 30390. 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 25079, 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 30388* | Lemma for ubth 30390. 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 30389* | Lemma for ubth 30390. Prove the reverse implication, using nmblolbi 30317. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) β β’ (π β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π)) | ||
Theorem | ubth 30390* | 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 30391* | Lemma for minveco 30401. 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 30392* | Lemma for minveco 30401. 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 30393* | Lemma for minveco 30401. 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 30394* | Lemma for minveco 30401. πΉ 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 30395* | Lemma for minveco 30401. 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 30396* | Lemma for minveco 30401. 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 30397* | Lemma for minveco 30401. 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))) β β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minvecolem5 30398* | Lemma for minveco 30401. Discharge the assumption about the sequence πΉ by applying countable choice ax-cc 10433. (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(π , β, < ) β β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minvecolem6 30399* | Lemma for minveco 30401. Any minimal point is less than π away from π΄. (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(π , β, < ) β β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)))) | ||
Theorem | minvecolem7 30400* | Lemma for minveco 30401. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) β β’ (π β β!π₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |