Home | Metamath
Proof Explorer Theorem List (p. 246 of 470) | < 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: | Metamath Proof Explorer
(1-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cphassi 24501 | Associative law for the first argument of an inner product with scalar _π. (Contributed by AV, 17-Oct-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β ((i Β· π΅) , π΄) = (i Β· (π΅ , π΄))) | ||
Theorem | cphassir 24502 | "Associative" law for the second argument of an inner product with scalar _π. (Contributed by AV, 17-Oct-2021.) |
β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (π΄ , (i Β· π΅)) = (-i Β· (π΄ , π΅))) | ||
Theorem | cphpyth 24503 | The pythagorean theorem for a subcomplex 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. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008.) (Revised by SN, 22-Sep-2024.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ + = (+gβπ) & β’ π = (normβπ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ ((π β§ (π΄ , π΅) = 0) β ((πβ(π΄ + π΅))β2) = (((πβπ΄)β2) + ((πβπ΅)β2))) | ||
Theorem | tcphex 24504* | Lemma for tcphbas 24506 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π₯ β π β¦ (ββ(π₯ , π₯))) β V | ||
Theorem | tcphval 24505* | Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ πΊ = (π toNrmGrp (π₯ β π β¦ (ββ(π₯ , π₯)))) | ||
Theorem | tcphbas 24506 | The base set of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) β β’ π = (BaseβπΊ) | ||
Theorem | tchplusg 24507 | The addition operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ + = (+gβπ) β β’ + = (+gβπΊ) | ||
Theorem | tcphsub 24508 | The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ πΊ = (toβPreHilβπ) & β’ β = (-gβπ) β β’ β = (-gβπΊ) | ||
Theorem | tcphmulr 24509 | The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = (.rβπ) β β’ Β· = (.rβπΊ) | ||
Theorem | tcphsca 24510 | The scalar field of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ πΉ = (Scalarβπ) β β’ πΉ = (ScalarβπΊ) | ||
Theorem | tcphvsca 24511 | The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = ( Β·π βπ) β β’ Β· = ( Β·π βπΊ) | ||
Theorem | tcphip 24512 | The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = (Β·πβπ) β β’ Β· = (Β·πβπΊ) | ||
Theorem | tcphtopn 24513 | The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π· = (distβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ (π β π β π½ = (MetOpenβπ·)) | ||
Theorem | tcphphl 24514 | Augmentation of a subcomplex pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space (because all the original components are the same). (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) β β’ (π β PreHil β πΊ β PreHil) | ||
Theorem | tchnmfval 24515* | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπΊ) & β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ (π β Grp β π = (π₯ β π β¦ (ββ(π₯ , π₯)))) | ||
Theorem | tcphnmval 24516 | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπΊ) & β’ π = (Baseβπ) & β’ , = (Β·πβπ) β β’ ((π β Grp β§ π β π) β (πβπ) = (ββ(π , π))) | ||
Theorem | cphtcphnm 24517 | The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπ) β β’ (π β βPreHil β π = (normβπΊ)) | ||
Theorem | tcphds 24518 | The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (normβπΊ) & β’ β = (-gβπ) β β’ (π β Grp β (π β β ) = (distβπΊ)) | ||
Theorem | phclm 24519 | A pre-Hilbert space whose field of scalars is a restriction of the field of complex numbers is a subcomplex module. TODO: redundant hypotheses. (Contributed by Mario Carneiro, 16-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) β β’ (π β π β βMod) | ||
Theorem | tcphcphlem3 24520 | Lemma for tcphcph 24524: real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) β β’ ((π β§ π β π) β (π , π) β β) | ||
Theorem | ipcau2 24521* | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau 24525. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ π = (normβπΊ) & β’ πΆ = ((π , π) / (π , π)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (absβ(π , π)) β€ ((πβπ) Β· (πβπ))) | ||
Theorem | tcphcphlem1 24522* | Lemma for tcphcph 24524: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ββ((π β π) , (π β π))) β€ ((ββ(π , π)) + (ββ(π , π)))) | ||
Theorem | tcphcphlem2 24523* | Lemma for tcphcph 24524: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ (π β π β πΎ) & β’ (π β π β π) β β’ (π β (ββ((π Β· π) , (π Β· π))) = ((absβπ) Β· (ββ(π , π)))) | ||
Theorem | tcphcph 24524* | The standard definition of a norm turns any pre-Hilbert space over a subfield of βfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) β β’ (π β πΊ β βPreHil) | ||
Theorem | ipcau 24525 | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. Part of Lemma 3.2-1(a) of [Kreyszig] p. 137. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 11-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π = (normβπ) β β’ ((π β βPreHil β§ π β π β§ π β π) β (absβ(π , π)) β€ ((πβπ) Β· (πβπ))) | ||
Theorem | nmparlem 24526 | Lemma for nmpar 24527. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | nmpar 24527 | A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π = (normβπ) β β’ ((π β βPreHil β§ π΄ β π β§ π΅ β π) β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | cphipval2 24528 | Value of the inner product expressed by the norm defined by it. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) = (((((πβ(π΄ + π΅))β2) β ((πβ(π΄ β π΅))β2)) + (i Β· (((πβ(π΄ + (i Β· π΅)))β2) β ((πβ(π΄ β (i Β· π΅)))β2)))) / 4)) | ||
Theorem | 4cphipval2 24529 | Four times the inner product value cphipval2 24528. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 18-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ β = (-gβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (4 Β· (π΄ , π΅)) = ((((πβ(π΄ + π΅))β2) β ((πβ(π΄ β π΅))β2)) + (i Β· (((πβ(π΄ + (i Β· π΅)))β2) β ((πβ(π΄ β (i Β· π΅)))β2))))) | ||
Theorem | cphipval 24530* | Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) β β’ (((π β βPreHil β§ i β πΎ) β§ π΄ β π β§ π΅ β π) β (π΄ , π΅) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄ + ((iβπ) Β· π΅)))β2)) / 4)) | ||
Theorem | ipcnlem2 24531 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π· = (distβπ) & β’ π = (normβπ) & β’ π = ((π / 2) / ((πβπ΄) + 1)) & β’ π = ((π / 2) / ((πβπ΅) + π)) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β+) & β’ (π β π β π) & β’ (π β π β π) & β’ (π β (π΄π·π) < π) & β’ (π β (π΅π·π) < π) β β’ (π β (absβ((π΄ , π΅) β (π , π))) < π ) | ||
Theorem | ipcnlem1 24532* | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ , = (Β·πβπ) & β’ π· = (distβπ) & β’ π = (normβπ) & β’ π = ((π / 2) / ((πβπ΄) + 1)) & β’ π = ((π / 2) / ((πβπ΅) + π)) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β π β β+) β β’ (π β βπ β β+ βπ₯ β π βπ¦ β π (((π΄π·π₯) < π β§ (π΅π·π¦) < π) β (absβ((π΄ , π΅) β (π₯ , π¦))) < π )) | ||
Theorem | ipcn 24533 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ , = (Β·ifβπ) & β’ π½ = (TopOpenβπ) & β’ πΎ = (TopOpenββfld) β β’ (π β βPreHil β , β ((π½ Γt π½) Cn πΎ)) | ||
Theorem | cnmpt1ip 24534* | Continuity of inner product; analogue of cnmpt12f 22940 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π½ = (TopOpenβπ) & β’ πΆ = (TopOpenββfld) & β’ , = (Β·πβπ) & β’ (π β π β βPreHil) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn π½)) & β’ (π β (π₯ β π β¦ π΅) β (πΎ Cn π½)) β β’ (π β (π₯ β π β¦ (π΄ , π΅)) β (πΎ Cn πΆ)) | ||
Theorem | cnmpt2ip 24535* | Continuity of inner product; analogue of cnmpt22f 22949 which cannot be used directly because Β·π is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π½ = (TopOpenβπ) & β’ πΆ = (TopOpenββfld) & β’ , = (Β·πβπ) & β’ (π β π β βPreHil) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt πΏ) Cn π½)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΎ Γt πΏ) Cn π½)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄ , π΅)) β ((πΎ Γt πΏ) Cn πΆ)) | ||
Theorem | csscld 24536 | A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ πΆ = (ClSubSpβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β βPreHil β§ π β πΆ) β π β (Clsdβπ½)) | ||
Theorem | clsocv 24537 | The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (Baseβπ) & β’ π = (ocvβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β βPreHil β§ π β π) β (πβ((clsβπ½)βπ)) = (πβπ)) | ||
Theorem | cphsscph 24538 | A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 25-Sep-2022.) |
β’ π = (π βΎs π) & β’ π = (LSubSpβπ) β β’ ((π β βPreHil β§ π β π) β π β βPreHil) | ||
Syntax | ccfil 24539 | Extend class notation with the class of Cauchy filters. |
class CauFil | ||
Syntax | ccau 24540 | Extend class notation with the class of Cauchy sequences. |
class Cau | ||
Syntax | ccmet 24541 | Extend class notation with the class of complete metrics. |
class CMet | ||
Definition | df-cfil 24542* | Define the set of Cauchy filters on a given extended metric space. A Cauchy filter is a filter on the set such that for every 0 < π₯ there is an element of the filter whose metric diameter is less than π₯. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ CauFil = (π β βͺ ran βMet β¦ {π β (Filβdom dom π) β£ βπ₯ β β+ βπ¦ β π (π β (π¦ Γ π¦)) β (0[,)π₯)}) | ||
Definition | df-cau 24543* | Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006.) |
β’ Cau = (π β βͺ ran βMet β¦ {π β (dom dom π βpm β) β£ βπ₯ β β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ)π₯)}) | ||
Definition | df-cmet 24544* | Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014.) |
β’ CMet = (π₯ β V β¦ {π β (Metβπ₯) β£ βπ β (CauFilβπ)((MetOpenβπ) fLim π) β β }) | ||
Theorem | lmmbr 24545* | Express the binary relation "sequence πΉ converges to point π " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition πΉ β (β Γ π) allows to use objects more general than sequences when convenient; see the comment in df-lm 22503. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) | ||
Theorem | lmmbr2 24546* | Express the binary relation "sequence πΉ converges to point π " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition πΉ β (β Γ π) allows to use objects more general than sequences when convenient; see the comment in df-lm 22503. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) | ||
Theorem | lmmbr3 24547* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) | ||
Theorem | lmmcvg 24548* | Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)(π΄ β π β§ (π΄π·π) < π )) | ||
Theorem | lmmbrf 24549* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 24546 presupposes that πΉ is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯))) | ||
Theorem | lmnn 24550* | A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((πΉβπ)π·π) < (1 / π)) β β’ (π β πΉ(βπ‘βπ½)π) | ||
Theorem | cfilfval 24551* | The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (CauFilβπ·) = {π β (Filβπ) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) | ||
Theorem | iscfil 24552* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | iscfil2 24553* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) | ||
Theorem | cfilfil 24554 | A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β πΉ β (Filβπ)) | ||
Theorem | cfili 24555* | Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β πΉ βπ¦ β π₯ βπ§ β π₯ (π¦π·π§) < π ) | ||
Theorem | cfil3i 24556* | A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β π (π₯(ballβπ·)π ) β πΉ) | ||
Theorem | cfilss 24557 | A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β πΊ β (CauFilβπ·)) | ||
Theorem | fgcfil 24558* | The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β ((πfilGenπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) | ||
Theorem | fmcfil 24559* | The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) | ||
Theorem | iscfil3 24560* | A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ β β+ βπ₯ β π (π₯(ballβπ·)π) β πΉ))) | ||
Theorem | cfilfcls 24561 | Similar to ultrafilters (uffclsflim 23305), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ π = dom dom π· β β’ (πΉ β (CauFilβπ·) β (π½ fClus πΉ) = (π½ fLim πΉ)) | ||
Theorem | caufval 24562* | The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.) |
β’ (π· β (βMetβπ) β (Cauβπ·) = {π β (π βpm β) β£ βπ₯ β β+ βπ β β€ (π βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πβπ)(ballβπ·)π₯)}) | ||
Theorem | iscau 24563* | Express the property "πΉ is a Cauchy sequence of metric π·". Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition πΉ β (β Γ π) allows to use objects more general than sequences when convenient; see the comment in df-lm 22503. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯)))) | ||
Theorem | iscau2 24564* | Express the property "πΉ is a Cauchy sequence of metric π· " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·(πΉβπ)) < π₯)))) | ||
Theorem | iscau3 24565* | Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β β€) β β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ βπ β (β€β₯βπ)((πΉβπ)π·(πΉβπ)) < π₯)))) | ||
Theorem | iscau4 24566* | Express the property "πΉ is a Cauchy sequence of metric π· " using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β (πΉβπ) = π΅) β β’ (π β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π β dom πΉ β§ π΄ β π β§ (π΄π·π΅) < π₯)))) | ||
Theorem | iscauf 24567* | Express the property "πΉ is a Cauchy sequence of metric π· " presupposing πΉ is a function. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
β’ π = (β€β₯βπ) & β’ (π β π· β (βMetβπ)) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ ((π β§ π β π) β (πΉβπ) = π΅) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ β (Cauβπ·) β βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΅π·π΄) < π₯)) | ||
Theorem | caun0 24568 | A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β π β β ) | ||
Theorem | caufpm 24569 | Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
β’ ((π· β (βMetβπ) β§ πΉ β (Cauβπ·)) β πΉ β (π βpm β)) | ||
Theorem | caucfil 24570 | A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ πΏ = ((π FilMap πΉ)β(β€β₯ β π)) β β’ ((π· β (βMetβπ) β§ π β β€ β§ πΉ:πβΆπ) β (πΉ β (Cauβπ·) β πΏ β (CauFilβπ·))) | ||
Theorem | iscmet 24571* | The property "π· is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014.) (Revised by Mario Carneiro, 13-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (CMetβπ) β (π· β (Metβπ) β§ βπ β (CauFilβπ·)(π½ fLim π) β β )) | ||
Theorem | cmetcvg 24572 | The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ πΉ β (CauFilβπ·)) β (π½ fLim πΉ) β β ) | ||
Theorem | cmetmet 24573 | A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 29-Jan-2014.) |
β’ (π· β (CMetβπ) β π· β (Metβπ)) | ||
Theorem | cmetmeti 24574 | A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.) |
β’ π· β (CMetβπ) β β’ π· β (Metβπ) | ||
Theorem | cmetcaulem 24575* | Lemma for cmetcau 24576. (Contributed by Mario Carneiro, 14-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ (π β π β π) & β’ (π β πΉ β (Cauβπ·)) & β’ πΊ = (π₯ β β β¦ if(π₯ β dom πΉ, (πΉβπ₯), π)) β β’ (π β πΉ β dom (βπ‘βπ½)) | ||
Theorem | cmetcau 24576 | The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ πΉ β (Cauβπ·)) β πΉ β dom (βπ‘βπ½)) | ||
Theorem | iscmet3lem3 24577* | Lemma for iscmet3 24580. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ π β β+) β βπ β π βπ β (β€β₯βπ)((1 / 2)βπ) < π ) | ||
Theorem | iscmet3lem1 24578* | Lemma for iscmet3 24580. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) & β’ (π β βπ β π βπ β (π...π)(πΉβπ) β (πβπ)) β β’ (π β πΉ β (Cauβπ·)) | ||
Theorem | iscmet3lem2 24579* | Lemma for iscmet3 24580. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) & β’ (π β βπ β π βπ β (π...π)(πΉβπ) β (πβπ)) & β’ (π β πΊ β (Filβπ)) & β’ (π β π:β€βΆπΊ) & β’ (π β πΉ β dom (βπ‘βπ½)) β β’ (π β (π½ fLim πΊ) β β ) | ||
Theorem | iscmet3 24580* | The property "π· is a complete metric" expressed in terms of functions on β (or any other upper integer set). Thus, we only have to look at functions on β, and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 5-May-2014.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) β β’ (π β (π· β (CMetβπ) β βπ β (Cauβπ·)(π:πβΆπ β π β dom (βπ‘βπ½)))) | ||
Theorem | iscmet2 24581 | A metric π· is complete iff all Cauchy sequences converge to a point in the space. The proof uses countable choice. Part of Definition 1.4-3 of [Kreyszig] p. 28. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (CMetβπ) β (π· β (Metβπ) β§ (Cauβπ·) β dom (βπ‘βπ½))) | ||
Theorem | cfilresi 24582 | A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβ(π· βΎ (π Γ π)))) β (πfilGenπΉ) β (CauFilβπ·)) | ||
Theorem | cfilres 24583 | Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ β (CauFilβπ·) β (πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))))) | ||
Theorem | caussi 24584 | Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ (π· β (βMetβπ) β (Cauβ(π· βΎ (π Γ π))) β (Cauβπ·)) | ||
Theorem | causs 24585 | Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ ((π· β (βMetβπ) β§ πΉ:ββΆπ) β (πΉ β (Cauβπ·) β πΉ β (Cauβ(π· βΎ (π Γ π))))) | ||
Theorem | equivcfil 24586* | If the metric π· is "strongly finer" than πΆ (meaning that there is a positive real constant π such that πΆ(π₯, π¦) β€ π Β· π·(π₯, π¦)), all the π·-Cauchy filters are also πΆ-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) β β’ (π β (CauFilβπ·) β (CauFilβπΆ)) | ||
Theorem | equivcau 24587* | If the metric π· is "strongly finer" than πΆ (meaning that there is a positive real constant π such that πΆ(π₯, π¦) β€ π Β· π·(π₯, π¦)), all the π·-Cauchy sequences are also πΆ-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.) |
β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) β β’ (π β (Cauβπ·) β (CauβπΆ)) | ||
Theorem | lmle 24588* | If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. (Contributed by NM, 23-Dec-2007.) (Proof shortened by Mario Carneiro, 1-May-2014.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β β€) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β π) & β’ (π β π β β*) & β’ ((π β§ π β π) β (ππ·(πΉβπ)) β€ π ) β β’ (π β (ππ·π) β€ π ) | ||
Theorem | nglmle 24589* | If the norm of each member of a converging sequence is less than or equal to a given amount, so is the norm of the convergence value. (Contributed by NM, 25-Dec-2007.) (Revised by AV, 16-Oct-2021.) |
β’ π = (BaseβπΊ) & β’ π· = ((distβπΊ) βΎ (π Γ π)) & β’ π½ = (MetOpenβπ·) & β’ π = (normβπΊ) & β’ (π β πΊ β NrmGrp) & β’ (π β πΉ:ββΆπ) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β β*) & β’ ((π β§ π β β) β (πβ(πΉβπ)) β€ π ) β β’ (π β (πβπ) β€ π ) | ||
Theorem | lmclim 24590 | Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (TopOpenββfld) & β’ π = (β€β₯βπ) β β’ ((π β β€ β§ π β dom πΉ) β (πΉ(βπ‘βπ½)π β (πΉ β (β βpm β) β§ πΉ β π))) | ||
Theorem | lmclimf 24591 | Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (TopOpenββfld) & β’ π = (β€β₯βπ) β β’ ((π β β€ β§ πΉ:πβΆβ) β (πΉ(βπ‘βπ½)π β πΉ β π)) | ||
Theorem | metelcls 24592* | A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. This proof uses countable choice ax-cc 10305. The statement can be generalized to first-countable spaces, not just metrizable spaces. (Contributed by NM, 8-Nov-2007.) (Proof shortened by Mario Carneiro, 1-May-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) β β’ (π β (π β ((clsβπ½)βπ) β βπ(π:ββΆπ β§ π(βπ‘βπ½)π))) | ||
Theorem | metcld 24593* | A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of [Kreyszig] p. 30. (Contributed by NM, 11-Nov-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π β π) β (π β (Clsdβπ½) β βπ₯βπ((π:ββΆπ β§ π(βπ‘βπ½)π₯) β π₯ β π))) | ||
Theorem | metcld2 24594 | A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of [Kreyszig] p. 30. (Contributed by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π β π) β (π β (Clsdβπ½) β ((βπ‘βπ½) β (π βm β)) β π)) | ||
Theorem | caubl 24595* | Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ (π β π· β (βMetβπ)) & β’ (π β πΉ:ββΆ(π Γ β+)) & β’ (π β βπ β β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ))) & β’ (π β βπ β β+ βπ β β (2nd β(πΉβπ)) < π) β β’ (π β (1st β πΉ) β (Cauβπ·)) | ||
Theorem | caublcls 24596* | The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ (π β π· β (βMetβπ)) & β’ (π β πΉ:ββΆ(π Γ β+)) & β’ (π β βπ β β ((ballβπ·)β(πΉβ(π + 1))) β ((ballβπ·)β(πΉβπ))) & β’ π½ = (MetOpenβπ·) β β’ ((π β§ (1st β πΉ)(βπ‘βπ½)π β§ π΄ β β) β π β ((clsβπ½)β((ballβπ·)β(πΉβπ΄)))) | ||
Theorem | metcnp4 24597* | Two ways to say a mapping from metric πΆ to metric π· is continuous at point π. Theorem 14-4.3 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 4-May-2014.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ (π β πΆ β (βMetβπ)) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) β β’ (π β (πΉ β ((π½ CnP πΎ)βπ) β (πΉ:πβΆπ β§ βπ((π:ββΆπ β§ π(βπ‘βπ½)π) β (πΉ β π)(βπ‘βπΎ)(πΉβπ))))) | ||
Theorem | metcn4 24598* | Two ways to say a mapping from metric πΆ to metric π· is continuous. Theorem 10.3 of [Munkres] p. 128. (Contributed by NM, 13-Jun-2007.) (Revised by Mario Carneiro, 4-May-2014.) |
β’ π½ = (MetOpenβπΆ) & β’ πΎ = (MetOpenβπ·) & β’ (π β πΆ β (βMetβπ)) & β’ (π β π· β (βMetβπ)) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ β (π½ Cn πΎ) β βπ(π:ββΆπ β βπ₯(π(βπ‘βπ½)π₯ β (πΉ β π)(βπ‘βπΎ)(πΉβπ₯))))) | ||
Theorem | iscmet3i 24599* | Properties that determine a complete metric space. (Contributed by NM, 15-Apr-2007.) (Revised by Mario Carneiro, 5-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ π· β (Metβπ) & β’ ((π β (Cauβπ·) β§ π:ββΆπ) β π β dom (βπ‘βπ½)) β β’ π· β (CMetβπ) | ||
Theorem | lmcau 24600 | Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. (Contributed by NM, 29-Jan-2008.) (Proof shortened by Mario Carneiro, 5-May-2014.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (βMetβπ) β dom (βπ‘βπ½) β (Cauβπ·)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |