![]() |
Metamath
Proof Explorer Theorem List (p. 251 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | ccfil 25001 | Extend class notation with the class of Cauchy filters. |
class CauFil | ||
Syntax | ccau 25002 | Extend class notation with the class of Cauchy sequences. |
class Cau | ||
Syntax | ccmet 25003 | Extend class notation with the class of complete metrics. |
class CMet | ||
Definition | df-cfil 25004* | 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 25005* | 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 25006* | 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 25007* | 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 22954. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ¦ β ran β€β₯(πΉ βΎ π¦):π¦βΆ(π(ballβπ·)π₯)))) | ||
Theorem | lmmbr2 25008* | 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 22954. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) β β’ (π β (πΉ(βπ‘βπ½)π β (πΉ β (π βpm β) β§ π β π β§ βπ₯ β β+ βπ β β€ βπ β (β€β₯βπ)(π β dom πΉ β§ (πΉβπ) β π β§ ((πΉβπ)π·π) < π₯)))) | ||
Theorem | lmmbr3 25009* | 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 25010* | Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ(βπ‘βπ½)π) & β’ (π β π β β+) β β’ (π β βπ β π βπ β (β€β₯βπ)(π΄ β π β§ (π΄π·π) < π )) | ||
Theorem | lmmbrf 25011* | Express the binary relation "sequence πΉ converges to point π " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 25008 presupposes that πΉ is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ ((π β§ π β π) β (πΉβπ) = π΄) & β’ (π β πΉ:πβΆπ) β β’ (π β (πΉ(βπ‘βπ½)π β (π β π β§ βπ₯ β β+ βπ β π βπ β (β€β₯βπ)(π΄π·π) < π₯))) | ||
Theorem | lmnn 25012* | A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (βMetβπ)) & β’ (π β π β π) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((πΉβπ)π·π) < (1 / π)) β β’ (π β πΉ(βπ‘βπ½)π) | ||
Theorem | cfilfval 25013* | The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (CauFilβπ·) = {π β (Filβπ) β£ βπ₯ β β+ βπ¦ β π (π· β (π¦ Γ π¦)) β (0[,)π₯)}) | ||
Theorem | iscfil 25014* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ (π· β (π¦ Γ π¦)) β (0[,)π₯)))) | ||
Theorem | iscfil2 25015* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (π· β (βMetβπ) β (πΉ β (CauFilβπ·) β (πΉ β (Filβπ) β§ βπ₯ β β+ βπ¦ β πΉ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯))) | ||
Theorem | cfilfil 25016 | A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β πΉ β (Filβπ)) | ||
Theorem | cfili 25017* | Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β πΉ βπ¦ β π₯ βπ§ β π₯ (π¦π·π§) < π ) | ||
Theorem | cfil3i 25018* | A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (CauFilβπ·) β§ π β β+) β βπ₯ β π (π₯(ballβπ·)π ) β πΉ) | ||
Theorem | cfilss 25019 | A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ (((π· β (βMetβπ) β§ πΉ β (CauFilβπ·)) β§ (πΊ β (Filβπ) β§ πΉ β πΊ)) β πΊ β (CauFilβπ·)) | ||
Theorem | fgcfil 25020* | The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ)) β ((πfilGenπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ (π§π·π€) < π₯)) | ||
Theorem | fmcfil 25021* | The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ π΅ β (fBasβπ) β§ πΉ:πβΆπ) β (((π FilMap πΉ)βπ΅) β (CauFilβπ·) β βπ₯ β β+ βπ¦ β π΅ βπ§ β π¦ βπ€ β π¦ ((πΉβπ§)π·(πΉβπ€)) < π₯)) | ||
Theorem | iscfil3 25022* | 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 25023 | Similar to ultrafilters (uffclsflim 23756), 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 25024* | 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 25025* | 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 22954. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
β’ (π· β (βMetβπ) β (πΉ β (Cauβπ·) β (πΉ β (π βpm β) β§ βπ₯ β β+ βπ β β€ (πΉ βΎ (β€β₯βπ)):(β€β₯βπ)βΆ((πΉβπ)(ballβπ·)π₯)))) | ||
Theorem | iscau2 25026* | 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 25027* | 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 25028* | 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 25029* | 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 25030 | 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 25031 | 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 25032 | 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 25033* | 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 25034 | The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ πΉ β (CauFilβπ·)) β (π½ fLim πΉ) β β ) | ||
Theorem | cmetmet 25035 | 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 25036 | A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.) |
β’ π· β (CMetβπ) β β’ π· β (Metβπ) | ||
Theorem | cmetcaulem 25037* | Lemma for cmetcau 25038. (Contributed by Mario Carneiro, 14-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ (π β π β π) & β’ (π β πΉ β (Cauβπ·)) & β’ πΊ = (π₯ β β β¦ if(π₯ β dom πΉ, (πΉβπ₯), π)) β β’ (π β πΉ β dom (βπ‘βπ½)) | ||
Theorem | cmetcau 25038 | 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 25039* | Lemma for iscmet3 25042. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) β β’ ((π β β€ β§ π β β+) β βπ β π βπ β (β€β₯βπ)((1 / 2)βπ) < π ) | ||
Theorem | iscmet3lem1 25040* | Lemma for iscmet3 25042. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) & β’ (π β βπ β π βπ β (π...π)(πΉβπ) β (πβπ)) β β’ (π β πΉ β (Cauβπ·)) | ||
Theorem | iscmet3lem2 25041* | Lemma for iscmet3 25042. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ π½ = (MetOpenβπ·) & β’ (π β π β β€) & β’ (π β π· β (Metβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β βπ β β€ βπ’ β (πβπ)βπ£ β (πβπ)(π’π·π£) < ((1 / 2)βπ)) & β’ (π β βπ β π βπ β (π...π)(πΉβπ) β (πβπ)) & β’ (π β πΊ β (Filβπ)) & β’ (π β π:β€βΆπΊ) & β’ (π β πΉ β dom (βπ‘βπ½)) β β’ (π β (π½ fLim πΊ) β β ) | ||
Theorem | iscmet3 25042* | 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 25043 | 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 25044 | 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 25045 | Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π· β (βMetβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β (πΉ β (CauFilβπ·) β (πΉ βΎt π) β (CauFilβ(π· βΎ (π Γ π))))) | ||
Theorem | caussi 25046 | Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ (π· β (βMetβπ) β (Cauβ(π· βΎ (π Γ π))) β (Cauβπ·)) | ||
Theorem | causs 25047 | Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
β’ ((π· β (βMetβπ) β§ πΉ:ββΆπ) β (πΉ β (Cauβπ·) β πΉ β (Cauβ(π· βΎ (π Γ π))))) | ||
Theorem | equivcfil 25048* | 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 25049* | 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 25050* | 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 25051* | 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 25052 | 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 25053 | 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 25054* | 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 10434. 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 25055* | 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 25056 | 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 25057* | 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 25058* | 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 25059* | 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 25060* | 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 25061* | 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 25062 | 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 25063 | Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (βMetβπ) β§ π΄ β (π½ fLim πΉ)) β πΉ β (CauFilβπ·)) | ||
Theorem | metsscmetcld 25064 | A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss 25065. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 9-Oct-2022.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (Metβπ) β§ (π· βΎ (π Γ π)) β (CMetβπ)) β π β (Clsdβπ½)) | ||
Theorem | cmetss 25065 | A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of [Kreyszig] p. 30. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 9-Oct-2022.) |
β’ π½ = (MetOpenβπ·) β β’ (π· β (CMetβπ) β ((π· βΎ (π Γ π)) β (CMetβπ) β π β (Clsdβπ½))) | ||
Theorem | equivcmet 25066* | If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau 25049, metss2 24242, this theorem does not have a one-directional form - it is possible for a metric πΆ that is strongly finer than the complete metric π· to be incomplete and vice versa. Consider π· = the metric on β induced by the usual homeomorphism from (0, 1) against the usual metric πΆ on β and against the discrete metric πΈ on β. Then both πΆ and πΈ are complete but π· is not, and πΆ is strongly finer than π·, which is strongly finer than πΈ. (Contributed by Mario Carneiro, 15-Sep-2015.) |
β’ (π β πΆ β (Metβπ)) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ (π β π β β+) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯πΆπ¦) β€ (π Β· (π₯π·π¦))) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯π·π¦) β€ (π Β· (π₯πΆπ¦))) β β’ (π β (πΆ β (CMetβπ) β π· β (CMetβπ))) | ||
Theorem | relcmpcmet 25067* | If π· is a metric space such that all the balls of some fixed size are relatively compact, then π· is complete. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π β β+) & β’ ((π β§ π₯ β π) β (π½ βΎt ((clsβπ½)β(π₯(ballβπ·)π ))) β Comp) β β’ (π β π· β (CMetβπ)) | ||
Theorem | cmpcmet 25068 | A compact metric space is complete. One half of heibor 36993. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (Metβπ)) & β’ (π β π½ β Comp) β β’ (π β π· β (CMetβπ)) | ||
Theorem | cfilucfil3 25069 | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (βMetβπ)) β ((πΆ β (Filβπ) β§ πΆ β (CauFiluβ(metUnifβπ·))) β πΆ β (CauFilβπ·))) | ||
Theorem | cfilucfil4 25070 | Given a metric π· and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.) |
β’ ((π β β β§ π· β (βMetβπ) β§ πΆ β (Filβπ)) β (πΆ β (CauFiluβ(metUnifβπ·)) β πΆ β (CauFilβπ·))) | ||
Theorem | cncmet 25071 | The set of complex numbers is a complete metric space under the absolute value metric. (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ π· = (abs β β ) β β’ π· β (CMetββ) | ||
Theorem | recmet 25072 | The real numbers are a complete metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.) |
β’ ((abs β β ) βΎ (β Γ β)) β (CMetββ) | ||
Theorem | bcthlem1 25073* | Lemma for bcth 25078. Substitutions for the function πΉ. (Contributed by Mario Carneiro, 9-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) β β’ ((π β§ (π΄ β β β§ π΅ β (π Γ β+))) β (πΆ β (π΄πΉπ΅) β (πΆ β (π Γ β+) β§ (2nd βπΆ) < (1 / π΄) β§ ((clsβπ½)β((ballβπ·)βπΆ)) β (((ballβπ·)βπ΅) β (πβπ΄))))) | ||
Theorem | bcthlem2 25074* | Lemma for bcth 25078. The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β π β β+) & β’ (π β πΆ β π) & β’ (π β π:ββΆ(π Γ β+)) & β’ (π β (πβ1) = β¨πΆ, π β©) & β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) β β’ (π β βπ β β ((ballβπ·)β(πβ(π + 1))) β ((ballβπ·)β(πβπ))) | ||
Theorem | bcthlem3 25075* | Lemma for bcth 25078. The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (Contributed by Mario Carneiro, 7-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β π β β+) & β’ (π β πΆ β π) & β’ (π β π:ββΆ(π Γ β+)) & β’ (π β (πβ1) = β¨πΆ, π β©) & β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) β β’ ((π β§ (1st β π)(βπ‘βπ½)π₯ β§ π΄ β β) β π₯ β ((ballβπ·)β(πβπ΄))) | ||
Theorem | bcthlem4 25076* | Lemma for bcth 25078. Given any open ball (πΆ(ballβπ·)π ) as starting point (and in particular, a ball in int(βͺ ran π)), the limit point π₯ of the centers of the induced sequence of balls π is outside βͺ ran π. Note that a set π΄ has empty interior iff every nonempty open set π contains points outside π΄, i.e. (π β π΄) β β . (Contributed by Mario Carneiro, 7-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β π β β+) & β’ (π β πΆ β π) & β’ (π β π:ββΆ(π Γ β+)) & β’ (π β (πβ1) = β¨πΆ, π β©) & β’ (π β βπ β β (πβ(π + 1)) β (ππΉ(πβπ))) β β’ (π β ((πΆ(ballβπ·)π ) β βͺ ran π) β β ) | ||
Theorem | bcthlem5 25077* |
Lemma for bcth 25078. The proof makes essential use of the Axiom
of
Dependent Choice axdc4uz 13954, which in the form used here accepts a
"selection" function πΉ from each element of πΎ to a
nonempty
subset of πΎ, and the result function π maps
π(π + 1)
to an element of πΉ(π, π(π)). The trick here is thus in
the choice of πΉ and πΎ: we let πΎ be the
set of all tagged
nonempty open sets (tagged here meaning that we have a point and an
open set, in an ordered pair), and πΉ(π, β¨π₯, π§β©) gives the
set of all balls of size less than 1 / π, tagged by their
centers, whose closures fit within the given open set π§ and
miss
π(π).
Since π(π) is closed, π§ β π(π) is open and also nonempty, since π§ is nonempty and π(π) has empty interior. Then there is some ball contained in it, and hence our function πΉ is valid (it never maps to the empty set). Now starting at a point in the interior of βͺ ran π, DC gives us the function π all whose elements are constrained by πΉ acting on the previous value. (This is all proven in this lemma.) Now π is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 25074) and whose sizes tend to zero, since they are bounded above by 1 / π. Thus, the centers of these balls form a Cauchy sequence, and converge to a point π₯ (see bcthlem4 25076). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point π₯ must be in all these balls (see bcthlem3 25075) and hence misses each π(π), contradicting the fact that π₯ is in the interior of βͺ ran π (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014.) |
β’ π½ = (MetOpenβπ·) & β’ (π β π· β (CMetβπ)) & β’ πΉ = (π β β, π§ β (π Γ β+) β¦ {β¨π₯, πβ© β£ ((π₯ β π β§ π β β+) β§ (π < (1 / π) β§ ((clsβπ½)β(π₯(ballβπ·)π)) β (((ballβπ·)βπ§) β (πβπ))))}) & β’ (π β π:ββΆ(Clsdβπ½)) & β’ (π β βπ β β ((intβπ½)β(πβπ)) = β ) β β’ (π β ((intβπ½)ββͺ ran π) = β ) | ||
Theorem | bcth 25078* | Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, no open set in the metric space can be the countable union of rare closed subsets (where rare means having a closure with empty interior), so some subset πβπ must have a nonempty interior. Theorem 4.7-2 of [Kreyszig] p. 247. (The terminology "meager" and "nonmeager" is used by Kreyszig to replace Baire's "of the first category" and "of the second category." The latter terms are going out of favor to avoid confusion with category theory.) See bcthlem5 25077 for an overview of the proof. (Contributed by NM, 28-Oct-2007.) (Proof shortened by Mario Carneiro, 6-Jan-2014.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ π:ββΆ(Clsdβπ½) β§ ((intβπ½)ββͺ ran π) β β ) β βπ β β ((intβπ½)β(πβπ)) β β ) | ||
Theorem | bcth2 25079* | Baire's Category Theorem, version 2: If countably many closed sets cover π, then one of them has an interior. (Contributed by Mario Carneiro, 10-Jan-2014.) |
β’ π½ = (MetOpenβπ·) β β’ (((π· β (CMetβπ) β§ π β β ) β§ (π:ββΆ(Clsdβπ½) β§ βͺ ran π = π)) β βπ β β ((intβπ½)β(πβπ)) β β ) | ||
Theorem | bcth3 25080* | Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014.) |
β’ π½ = (MetOpenβπ·) β β’ ((π· β (CMetβπ) β§ π:ββΆπ½ β§ βπ β β ((clsβπ½)β(πβπ)) = π) β ((clsβπ½)ββ© ran π) = π) | ||
Syntax | ccms 25081 | Extend class notation with the class of complete metric spaces. |
class CMetSp | ||
Syntax | cbn 25082 | Extend class notation with the class of Banach spaces. |
class Ban | ||
Syntax | chl 25083 | Extend class notation with the class of subcomplex Hilbert spaces. |
class βHil | ||
Definition | df-cms 25084* | Define the class of complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ CMetSp = {π€ β MetSp β£ [(Baseβπ€) / π]((distβπ€) βΎ (π Γ π)) β (CMetβπ)} | ||
Definition | df-bn 25085 | Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ Ban = {π€ β (NrmVec β© CMetSp) β£ (Scalarβπ€) β CMetSp} | ||
Definition | df-hl 25086 | Define the class of all subcomplex Hilbert spaces. A subcomplex Hilbert space is a Banach space which is also an inner product space over a subfield of the field of complex numbers closed under square roots of nonnegative reals. (Contributed by Steve Rodriguez, 28-Apr-2007.) |
β’ βHil = (Ban β© βPreHil) | ||
Theorem | isbn 25087 | A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β Ban β (π β NrmVec β§ π β CMetSp β§ πΉ β CMetSp)) | ||
Theorem | bnsca 25088 | The scalar field of a Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ πΉ = (Scalarβπ) β β’ (π β Ban β πΉ β CMetSp) | ||
Theorem | bnnvc 25089 | A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β NrmVec) | ||
Theorem | bnnlm 25090 | A Banach space is a normed module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β NrmMod) | ||
Theorem | bnngp 25091 | A Banach space is a normed group. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β NrmGrp) | ||
Theorem | bnlmod 25092 | A Banach space is a left module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β LMod) | ||
Theorem | bncms 25093 | A Banach space is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β Ban β π β CMetSp) | ||
Theorem | iscms 25094 | A complete metric space is a metric space with a complete metric. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β CMetSp β (π β MetSp β§ π· β (CMetβπ))) | ||
Theorem | cmscmet 25095 | The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β CMetSp β π· β (CMetβπ)) | ||
Theorem | bncmet 25096 | The induced metric on Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.) |
β’ π = (Baseβπ) & β’ π· = ((distβπ) βΎ (π Γ π)) β β’ (π β Ban β π· β (CMetβπ)) | ||
Theorem | cmsms 25097 | A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (πΊ β CMetSp β πΊ β MetSp) | ||
Theorem | cmspropd 25098 | Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β ((distβπΎ) βΎ (π΅ Γ π΅)) = ((distβπΏ) βΎ (π΅ Γ π΅))) & β’ (π β (TopOpenβπΎ) = (TopOpenβπΏ)) β β’ (π β (πΎ β CMetSp β πΏ β CMetSp)) | ||
Theorem | cmssmscld 25099 | The restriction of a metric space is closed if it is complete. (Contributed by AV, 9-Oct-2022.) |
β’ πΎ = (π βΎs π΄) & β’ π = (Baseβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β MetSp β§ π΄ β π β§ πΎ β CMetSp) β π΄ β (Clsdβπ½)) | ||
Theorem | cmsss 25100 | The restriction of a complete metric space is complete iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ πΎ = (π βΎs π΄) & β’ π = (Baseβπ) & β’ π½ = (TopOpenβπ) β β’ ((π β CMetSp β§ π΄ β π) β (πΎ β CMetSp β π΄ β (Clsdβπ½))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |