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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cphassir 24501 | "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 24502 | 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 24503* | Lemma for tcphbas 24505 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) β β’ (π₯ β π β¦ (ββ(π₯ , π₯))) β V | ||
Theorem | tcphval 24504* | 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 24505 | 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 24506 | 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 24507 | 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 24508 | 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 24509 | 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 24510 | The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = ( Β·π βπ) β β’ Β· = ( Β·π βπΊ) | ||
Theorem | tcphip 24511 | The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ Β· = (Β·πβπ) β β’ Β· = (Β·πβπΊ) | ||
Theorem | tcphtopn 24512 | 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 24513 | 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 24514* | 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 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 | cphtcphnm 24516 | 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 24517 | 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 24518 | 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 24519 | Lemma for tcphcph 24523: 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 24520* | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau 24524. (Contributed by Mario Carneiro, 11-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ π = (normβπΊ) & β’ πΆ = ((π , π) / (π , π)) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (absβ(π , π)) β€ ((πβπ) Β· (πβπ))) | ||
Theorem | tcphcphlem1 24521* | Lemma for tcphcph 24523: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ β = (-gβπ) & β’ (π β π β π) & β’ (π β π β π) β β’ (π β (ββ((π β π) , (π β π))) β€ ((ββ(π , π)) + (ββ(π , π)))) | ||
Theorem | tcphcphlem2 24522* | Lemma for tcphcph 24523: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.) |
β’ πΊ = (toβPreHilβπ) & β’ π = (Baseβπ) & β’ πΉ = (Scalarβπ) & β’ (π β π β PreHil) & β’ (π β πΉ = (βfld βΎs πΎ)) & β’ , = (Β·πβπ) & β’ ((π β§ (π₯ β πΎ β§ π₯ β β β§ 0 β€ π₯)) β (ββπ₯) β πΎ) & β’ ((π β§ π₯ β π) β 0 β€ (π₯ , π₯)) & β’ πΎ = (BaseβπΉ) & β’ Β· = ( Β·π βπ) & β’ (π β π β πΎ) & β’ (π β π β π) β β’ (π β (ββ((π Β· π) , (π Β· π))) = ((absβπ) Β· (ββ(π , π)))) | ||
Theorem | tcphcph 24523* | 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 24524 | 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 24525 | Lemma for nmpar 24526. (Contributed by Mario Carneiro, 7-Oct-2015.) |
β’ π = (Baseβπ) & β’ + = (+gβπ) & β’ β = (-gβπ) & β’ π = (normβπ) & β’ , = (Β·πβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ (π β π β βPreHil) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β (((πβ(π΄ + π΅))β2) + ((πβ(π΄ β π΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | nmpar 24526 | 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 24527 | 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 24528 | Four times the inner product value cphipval2 24527. (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 24529* | 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 24530 | 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 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 | ipcn 24532 | 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 24533* | Continuity of inner product; analogue of cnmpt12f 22939 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 24534* | Continuity of inner product; analogue of cnmpt22f 22948 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 24535 | 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 24536 | 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 24537 | 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 24538 | Extend class notation with the class of Cauchy filters. |
class CauFil | ||
Syntax | ccau 24539 | Extend class notation with the class of Cauchy sequences. |
class Cau | ||
Syntax | ccmet 24540 | Extend class notation with the class of complete metrics. |
class CMet | ||
Definition | df-cfil 24541* | 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 24542* | 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 24543* | 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 24544* | 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 22502. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) | ||
Theorem | lmmbr2 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 22502. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) | ||
Theorem | lmmbr3 24546* | 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 24547* | Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)(π΄ β π β§ (π΄π·π) < π )) | ||
Theorem | lmmbrf 24548* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 24545 presupposes that πΉ is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯))) | ||
Theorem | lmnn 24549* | A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((πΉβπ)π·π) < (1 / π)) β β’ (π β πΉ(βπ‘βπ½)π) | ||
Theorem | cfilfval 24550* | The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (CauFilβπ·) = {π β (Filβπ) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) | ||
Theorem | iscfil 24551* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | iscfil2 24552* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) | ||
Theorem | cfilfil 24553 | A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β πΉ β (Filβπ)) | ||
Theorem | cfili 24554* | Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β πΉ βπ¦ β π₯ βπ§ β π₯ (π¦π·π§) < π ) | ||
Theorem | cfil3i 24555* | A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β π (π₯(ballβπ·)π ) β πΉ) | ||
Theorem | cfilss 24556 | A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β πΊ β (CauFilβπ·)) | ||
Theorem | fgcfil 24557* | The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β ((πfilGenπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) | ||
Theorem | fmcfil 24558* | The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) | ||
Theorem | iscfil3 24559* | 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 24560 | Similar to ultrafilters (uffclsflim 23304), 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 24561* | 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 24562* | 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 22502. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯)))) | ||
Theorem | iscau2 24563* | 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 24564* | 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 24565* | 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 24566* | 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 24567 | 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 24568 | 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 24569 | 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 24570* | 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 24571 | The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ πΉ β (CauFilβπ·)) β (π½ fLim πΉ) β β ) | ||
Theorem | cmetmet 24572 | 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 24573 | A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.) |
β’ π· β (CMetβπ) β β’ π· β (Metβπ) | ||
Theorem | cmetcaulem 24574* | Lemma for cmetcau 24575. (Contributed by Mario Carneiro, 14-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ (π β π β π) & β’ (π β πΉ β (Cauβπ·)) & β’ πΊ = (π₯ β β β¦ if(π₯ β dom πΉ, (πΉβπ₯), π)) β β’ (π β πΉ β dom (βπ‘βπ½)) | ||
Theorem | cmetcau 24575 | 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 24576* | Lemma for iscmet3 24579. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ π β β+) β βπ β π βπ β (β€β₯βπ)((1 / 2)βπ) < π ) | ||
Theorem | iscmet3lem1 24577* | Lemma for iscmet3 24579. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) & β’ (π β βπ β π βπ β (π...π)(πΉβπ) β (πβπ)) β β’ (π β πΉ β (Cauβπ·)) | ||
Theorem | iscmet3lem2 24578* | Lemma for iscmet3 24579. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) & β’ (π β βπ β π βπ β (π...π)(πΉβπ) β (πβπ)) & β’ (π β πΊ β (Filβπ)) & β’ (π β π:β€βΆπΊ) & β’ (π β πΉ β dom (βπ‘βπ½)) β β’ (π β (π½ fLim πΊ) β β ) | ||
Theorem | iscmet3 24579* | 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 24580 | 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 24581 | 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 24582 | Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ β (CauFilβπ·) β (πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))))) | ||
Theorem | caussi 24583 | Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ (π· β (βMetβπ) β (Cauβ(π· βΎ (π Γ π))) β (Cauβπ·)) | ||
Theorem | causs 24584 | Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ ((π· β (βMetβπ) β§ πΉ:ββΆπ) β (πΉ β (Cauβπ·) β πΉ β (Cauβ(π· βΎ (π Γ π))))) | ||
Theorem | equivcfil 24585* | 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 24586* | 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 24587* | 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 24588* | 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 24589 | 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 24590 | 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 24591* | 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 24592* | 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 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 Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π β π) β (π β (Clsdβπ½) β ((βπ‘βπ½) β (π βm β)) β π)) | ||
Theorem | caubl 24594* | 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 24595* | 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 24596* | 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 24597* | 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 24598* | 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 24599 | 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βπ·)) | ||
Theorem | flimcfil 24600 | Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β πΉ β (CauFilβπ·)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |