![]() |
Metamath
Proof Explorer Theorem List (p. 236 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hausflf2 23501 | If a convergent function has its values in a Hausdorff space, then it has a unique limit. (Contributed by FL, 14-Nov-2010.) (Revised by Stefan O'Rear, 6-Aug-2015.) |
β’ π = βͺ π½ β β’ (((π½ β Haus β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ ((π½ fLimf πΏ)βπΉ) β β ) β ((π½ fLimf πΏ)βπΉ) β 1o) | ||
Theorem | cnpflfi 23502 | Forward direction of cnpflf 23504. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π΄ β (π½ fLim πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)) | ||
Theorem | cnpflf2 23503 | πΉ is continuous at point π΄ iff a limit of πΉ when π₯ tends to π΄ is (πΉβπ΄). Proposition 9 of [BourbakiTop1] p. TG I.50. (Contributed by FL, 29-May-2011.) (Revised by Mario Carneiro, 9-Apr-2015.) |
β’ πΏ = ((neiβπ½)β{π΄}) β β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ (πΉβπ΄) β ((πΎ fLimf πΏ)βπΉ)))) | ||
Theorem | cnpflf 23504* | Continuity of a function at a point in terms of filter limits. (Contributed by Jeff Hankins, 7-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fLim π) β (πΉβπ΄) β ((πΎ fLimf π)βπΉ))))) | ||
Theorem | cnflf 23505* | A function is continuous iff it respects filter limits. (Contributed by Jeff Hankins, 6-Sep-2009.) (Revised by Stefan O'Rear, 7-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)βπ₯ β (π½ fLim π)(πΉβπ₯) β ((πΎ fLimf π)βπΉ)))) | ||
Theorem | cnflf2 23506* | A function is continuous iff it respects filter limits. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)(πΉ β (π½ fLim π)) β ((πΎ fLimf π)βπΉ)))) | ||
Theorem | flfcnp 23507 | A continuous function preserves filter limits. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fLimf πΏ)βπΉ) β§ πΊ β ((π½ CnP πΎ)βπ΄))) β (πΊβπ΄) β ((πΎ fLimf πΏ)β(πΊ β πΉ))) | ||
Theorem | lmflf 23508 | The topological limit relation on functions can be written in terms of the filter limit along the filter generated by the upper integer sets. (Contributed by Mario Carneiro, 13-Oct-2015.) |
β’ π = (β€β₯βπ) & β’ πΏ = (πfilGen(β€β₯ β π)) β β’ ((π½ β (TopOnβπ) β§ π β β€ β§ πΉ:πβΆπ) β (πΉ(βπ‘βπ½)π β π β ((π½ fLimf πΏ)βπΉ))) | ||
Theorem | txflf 23509* | Two sequences converge in a filter iff the sequence of their ordered pairs converges. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (Filβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) & β’ π» = (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) β β’ (π β (β¨π , πβ© β (((π½ Γt πΎ) fLimf πΏ)βπ») β (π β ((π½ fLimf πΏ)βπΉ) β§ π β ((πΎ fLimf πΏ)βπΊ)))) | ||
Theorem | flfcnp2 23510* | The image of a convergent sequence under a continuous map is convergent to the image of the original point. Binary operation version. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (Filβπ)) & β’ ((π β§ π₯ β π) β π΄ β π) & β’ ((π β§ π₯ β π) β π΅ β π) & β’ (π β π β ((π½ fLimf πΏ)β(π₯ β π β¦ π΄))) & β’ (π β π β ((πΎ fLimf πΏ)β(π₯ β π β¦ π΅))) & β’ (π β π β (((π½ Γt πΎ) CnP π)ββ¨π , πβ©)) β β’ (π β (π ππ) β ((π fLimf πΏ)β(π₯ β π β¦ (π΄ππ΅)))) | ||
Theorem | fclsval 23511* | The set of all cluster points of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ β (Filβπ)) β (π½ fClus πΉ) = if(π = π, β© π‘ β πΉ ((clsβπ½)βπ‘), β )) | ||
Theorem | isfcls 23512* | A cluster point of a filter. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fClus πΉ) β (π½ β Top β§ πΉ β (Filβπ) β§ βπ β πΉ π΄ β ((clsβπ½)βπ ))) | ||
Theorem | fclsfil 23513 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fClus πΉ) β πΉ β (Filβπ)) | ||
Theorem | fclstop 23514 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π΄ β (π½ fClus πΉ) β π½ β Top) | ||
Theorem | fclstopon 23515 | Reverse closure for the cluster point predicate. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π΄ β (π½ fClus πΉ) β (π½ β (TopOnβπ) β πΉ β (Filβπ))) | ||
Theorem | isfcls2 23516* | A cluster point of a filter. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β βπ β πΉ π΄ β ((clsβπ½)βπ ))) | ||
Theorem | fclsopn 23517* | Write the cluster point condition in terms of open sets. (Contributed by Jeff Hankins, 10-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΉ (π β© π ) β β )))) | ||
Theorem | fclsopni 23518 | An open neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π΄ β (π½ fClus πΉ) β§ (π β π½ β§ π΄ β π β§ π β πΉ)) β (π β© π) β β ) | ||
Theorem | fclselbas 23519 | A cluster point is in the base set. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ π = βͺ π½ β β’ (π΄ β (π½ fClus πΉ) β π΄ β π) | ||
Theorem | fclsneii 23520 | A neighborhood of a cluster point of a filter intersects any element of that filter. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π΄ β (π½ fClus πΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΉ) β (π β© π) β β ) | ||
Theorem | fclssscls 23521 | The set of cluster points is a subset of the closure of any filter element. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π β πΉ β (π½ fClus πΉ) β ((clsβπ½)βπ)) | ||
Theorem | fclsnei 23522* | Cluster points in terms of neighborhoods. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΉ (π β© π ) β β ))) | ||
Theorem | supnfcls 23523* | The filter of supersets of π β π does not cluster at any point of the open set π. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ π β π½ β§ π΄ β π) β Β¬ π΄ β (π½ fClus {π₯ β π« π β£ (π β π) β π₯})) | ||
Theorem | fclsbas 23524* | Cluster points in terms of filter bases. (Contributed by Jeff Hankins, 13-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ πΉ = (πfilGenπ΅) β β’ ((π½ β (TopOnβπ) β§ π΅ β (fBasβπ)) β (π΄ β (π½ fClus πΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β π΅ (π β© π ) β β )))) | ||
Theorem | fclsss1 23525 | A finer topology has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π½ β πΎ) β (πΎ fClus πΉ) β (π½ fClus πΉ)) | ||
Theorem | fclsss2 23526 | A finer filter has fewer cluster points. (Contributed by Jeff Hankins, 11-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ πΉ β πΊ) β (π½ fClus πΊ) β (π½ fClus πΉ)) | ||
Theorem | fclsrest 23527 | The set of cluster points in a restricted topological space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ β (Filβπ) β§ π β πΉ) β ((π½ βΎt π) fClus (πΉ βΎt π)) = ((π½ fClus πΉ) β© π)) | ||
Theorem | fclscf 23528* | Characterization of fineness of topologies in terms of cluster points. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (π½ β πΎ β βπ β (Filβπ)(πΎ fClus π) β (π½ fClus π))) | ||
Theorem | flimfcls 23529 | A limit point is a cluster point. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π½ fLim πΉ) β (π½ fClus πΉ) | ||
Theorem | fclsfnflim 23530* | A filter clusters at a point iff a finer filter converges to it. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ (πΉ β (Filβπ) β (π΄ β (π½ fClus πΉ) β βπ β (Filβπ)(πΉ β π β§ π΄ β (π½ fLim π)))) | ||
Theorem | flimfnfcls 23531* | A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23530, this theorem illustrates the duality between convergence and clustering. (Contributed by Jeff Hankins, 12-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ (πΉ β (Filβπ) β (π΄ β (π½ fLim πΉ) β βπ β (Filβπ)(πΉ β π β π΄ β (π½ fClus π)))) | ||
Theorem | fclscmpi 23532 | Forward direction of fclscmp 23533. Every filter clusters in a compact space. (Contributed by Mario Carneiro, 11-Apr-2015.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ πΉ β (Filβπ)) β (π½ fClus πΉ) β β ) | ||
Theorem | fclscmp 23533* | A space is compact iff every filter clusters. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 8-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ β Comp β βπ β (Filβπ)(π½ fClus π) β β )) | ||
Theorem | uffclsflim 23534 | The cluster points of an ultrafilter are its limit points. (Contributed by Jeff Hankins, 11-Dec-2009.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ (πΉ β (UFilβπ) β (π½ fClus πΉ) = (π½ fLim πΉ)) | ||
Theorem | ufilcmp 23535* | A space is compact iff every ultrafilter converges. (Contributed by Jeff Hankins, 11-Dec-2009.) (Proof shortened by Mario Carneiro, 12-Apr-2015.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ ((π β UFL β§ π½ β (TopOnβπ)) β (π½ β Comp β βπ β (UFilβπ)(π½ fLim π) β β )) | ||
Theorem | fcfval 23536 | The set of cluster points of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fClusf πΏ)βπΉ) = (π½ fClus ((π FilMap πΉ)βπΏ))) | ||
Theorem | isfcf 23537* | The property of being a cluster point of a function. (Contributed by Jeff Hankins, 24-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β π½ (π΄ β π β βπ β πΏ (π β© (πΉ β π )) β β )))) | ||
Theorem | fcfnei 23538* | The property of being a cluster point of a function in terms of neighborhoods. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β (π΄ β ((π½ fClusf πΏ)βπΉ) β (π΄ β π β§ βπ β ((neiβπ½)β{π΄})βπ β πΏ (π β© (πΉ β π )) β β ))) | ||
Theorem | fcfelbas 23539 | A cluster point of a function is in the base set of the topology. (Contributed by Jeff Hankins, 26-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ π΄ β ((π½ fClusf πΏ)βπΉ)) β π΄ β π) | ||
Theorem | fcfneii 23540 | A neighborhood of a cluster point of a function contains a function value from every tail. (Contributed by Jeff Hankins, 27-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β§ (π΄ β ((π½ fClusf πΏ)βπΉ) β§ π β ((neiβπ½)β{π΄}) β§ π β πΏ)) β (π β© (πΉ β π)) β β ) | ||
Theorem | flfssfcf 23541 | A limit point of a function is a cluster point of the function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (Filβπ) β§ πΉ:πβΆπ) β ((π½ fLimf πΏ)βπΉ) β ((π½ fClusf πΏ)βπΉ)) | ||
Theorem | uffcfflf 23542 | If the domain filter is an ultrafilter, the cluster points of the function are the limit points. (Contributed by Jeff Hankins, 12-Dec-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΏ β (UFilβπ) β§ πΉ:πβΆπ) β ((π½ fClusf πΏ)βπΉ) = ((π½ fLimf πΏ)βπΉ)) | ||
Theorem | cnpfcfi 23543 | Lemma for cnpfcf 23544. If a function is continuous at a point, it respects clustering there. (Contributed by Jeff Hankins, 20-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((πΎ β Top β§ π΄ β (π½ fClus πΏ) β§ πΉ β ((π½ CnP πΎ)βπ΄)) β (πΉβπ΄) β ((πΎ fClusf πΏ)βπΉ)) | ||
Theorem | cnpfcf 23544* | A function πΉ is continuous at point π΄ iff πΉ respects cluster points there. (Contributed by Jeff Hankins, 14-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π΄ β π) β (πΉ β ((π½ CnP πΎ)βπ΄) β (πΉ:πβΆπ β§ βπ β (Filβπ)(π΄ β (π½ fClus π) β (πΉβπ΄) β ((πΎ fClusf π)βπΉ))))) | ||
Theorem | cnfcf 23545* | Continuity of a function in terms of cluster points of a function. (Contributed by Jeff Hankins, 28-Nov-2009.) (Revised by Stefan O'Rear, 9-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β (π½ Cn πΎ) β (πΉ:πβΆπ β§ βπ β (Filβπ)βπ₯ β (π½ fClus π)(πΉβπ₯) β ((πΎ fClusf π)βπΉ)))) | ||
Theorem | flfcntr 23546 | A continuous function's value is always in the trace of its filter limit. (Contributed by Thierry Arnoux, 30-Aug-2020.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β π΄ β πΆ) & β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) & β’ (π β π β π΄) β β’ (π β (πΉβπ) β ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) | ||
Theorem | alexsublem 23547* | Lemma for alexsub 23548. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π β π β UFL) & β’ (π β π = βͺ π΅) & β’ (π β π½ = (topGenβ(fiβπ΅))) & β’ ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) & β’ (π β πΉ β (UFilβπ)) & β’ (π β (π½ fLim πΉ) = β ) β β’ Β¬ π | ||
Theorem | alexsub 23548* | The Alexander Subbase Theorem: If π΅ is a subbase for the topology π½, and any cover taken from π΅ has a finite subcover, then the generated topology is compact. This proof uses the ultrafilter lemma; see alexsubALT 23554 for a proof using Zorn's lemma. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 26-Aug-2015.) |
β’ (π β π β UFL) & β’ (π β π = βͺ π΅) & β’ (π β π½ = (topGenβ(fiβπ΅))) & β’ ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) β β’ (π β π½ β Comp) | ||
Theorem | alexsubb 23549* | Biconditional form of the Alexander Subbase Theorem alexsub 23548. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ ((π β UFL β§ π = βͺ π΅) β ((topGenβ(fiβπ΅)) β Comp β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) | ||
Theorem | alexsubALTlem1 23550* | Lemma for alexsubALT 23554. A compact space has a subbase such that every cover taken from it has a finite subcover. (Contributed by Jeff Hankins, 27-Jan-2010.) |
β’ π = βͺ π½ β β’ (π½ β Comp β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) | ||
Theorem | alexsubALTlem2 23551* | Lemma for alexsubALT 23554. Every subset of a base which has no finite subcover is a subset of a maximal such collection. (Contributed by Jeff Hankins, 27-Jan-2010.) |
β’ π = βͺ π½ β β’ (((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ βπ β (π« π β© Fin) Β¬ π = βͺ π) β βπ’ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β })βπ£ β ({π§ β π« (fiβπ₯) β£ (π β π§ β§ βπ β (π« π§ β© Fin) Β¬ π = βͺ π)} βͺ {β }) Β¬ π’ β π£) | ||
Theorem | alexsubALTlem3 23552* | Lemma for alexsubALT 23554. If a point is covered by a collection taken from the base with no finite subcover, a set from the subbase can be added that covers the point so that the resulting collection has no finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.) |
β’ π = βͺ π½ β β’ (((((π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β§ π β π« (fiβπ₯)) β§ (π’ β π« (fiβπ₯) β§ (π β π’ β§ βπ β (π« π’ β© Fin) Β¬ π = βͺ π))) β§ π€ β π’) β§ ((π‘ β (π« π₯ β© Fin) β§ π€ = β© π‘) β§ (π¦ β π€ β§ Β¬ π¦ β βͺ (π₯ β© π’)))) β βπ β π‘ βπ β (π« (π’ βͺ {π }) β© Fin) Β¬ π = βͺ π) | ||
Theorem | alexsubALTlem4 23553* | Lemma for alexsubALT 23554. If any cover taken from a subbase has a finite subcover, any cover taken from the corresponding base has a finite subcover. (Contributed by Jeff Hankins, 28-Jan-2010.) (Revised by Mario Carneiro, 14-Dec-2013.) |
β’ π = βͺ π½ β β’ (π½ = (topGenβ(fiβπ₯)) β (βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π) β βπ β π« (fiβπ₯)(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) | ||
Theorem | alexsubALT 23554* | The Alexander Subbase Theorem: a space is compact iff it has a subbase such that any cover taken from the subbase has a finite subcover. (Contributed by Jeff Hankins, 24-Jan-2010.) (Revised by Mario Carneiro, 11-Feb-2015.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = βͺ π½ β β’ (π½ β Comp β βπ₯(π½ = (topGenβ(fiβπ₯)) β§ βπ β π« π₯(π = βͺ π β βπ β (π« π β© Fin)π = βͺ π))) | ||
Theorem | ptcmplem1 23555* | Lemma for ptcmp 23561. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) β β’ (π β (π = βͺ (ran π βͺ {π}) β§ (βtβπΉ) = (topGenβ(fiβ(ran π βͺ {π}))))) | ||
Theorem | ptcmplem2 23556* | Lemma for ptcmp 23561. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) β β’ (π β βͺ π β {π β π΄ β£ Β¬ βͺ (πΉβπ) β 1o}βͺ (πΉβπ) β dom card) | ||
Theorem | ptcmplem3 23557* | Lemma for ptcmp 23561. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) & β’ πΎ = {π’ β (πΉβπ) β£ (β‘(π€ β π β¦ (π€βπ)) β π’) β π} β β’ (π β βπ(π Fn π΄ β§ βπ β π΄ (πβπ) β (βͺ (πΉβπ) β βͺ πΎ))) | ||
Theorem | ptcmplem4 23558* | Lemma for ptcmp 23561. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) & β’ πΎ = {π’ β (πΉβπ) β£ (β‘(π€ β π β¦ (π€βπ)) β π’) β π} β β’ Β¬ π | ||
Theorem | ptcmplem5 23559* | Lemma for ptcmp 23561. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) β β’ (π β (βtβπΉ) β Comp) | ||
Theorem | ptcmpg 23560 | Tychonoff's theorem: The product of compact spaces is compact. The choice principles needed are encoded in the last hypothesis: the base set of the product must be well-orderable and satisfy the ultrafilter lemma. Both these assumptions are satisfied if π« π« π is well-orderable, so if we assume the Axiom of Choice we can eliminate them (see ptcmp 23561). (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π½ = (βtβπΉ) & β’ π = βͺ π½ β β’ ((π΄ β π β§ πΉ:π΄βΆComp β§ π β (UFL β© dom card)) β π½ β Comp) | ||
Theorem | ptcmp 23561 | Tychonoff's theorem: The product of compact spaces is compact. The proof uses the Axiom of Choice. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆComp) β (βtβπΉ) β Comp) | ||
Syntax | ccnext 23562 | Extend class notation with the continuous extension operation. |
class CnExt | ||
Definition | df-cnext 23563* | Define the continuous extension of a given function. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
β’ CnExt = (π β Top, π β Top β¦ (π β (βͺ π βpm βͺ π) β¦ βͺ π₯ β ((clsβπ)βdom π)({π₯} Γ ((π fLimf (((neiβπ)β{π₯}) βΎt dom π))βπ)))) | ||
Theorem | cnextval 23564* | The function applying continuous extension to a given function π. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
β’ ((π½ β Top β§ πΎ β Top) β (π½CnExtπΎ) = (π β (βͺ πΎ βpm βͺ π½) β¦ βͺ π₯ β ((clsβπ½)βdom π)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt dom π))βπ)))) | ||
Theorem | cnextfval 23565* | The continuous extension of a given function πΉ. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
β’ π = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β ((π½CnExtπΎ)βπΉ) = βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) | ||
Theorem | cnextrel 23566 | In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Rel ((π½CnExtπΎ)βπΉ)) | ||
Theorem | cnextfun 23567 | If the target space is Hausdorff, a continuous extension is a function. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Haus) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Fun ((π½CnExtπΎ)βπΉ)) | ||
Theorem | cnextfvval 23568* | The value of the continuous extension of a given function πΉ at a point π. (Contributed by Thierry Arnoux, 21-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) β β’ ((π β§ π β πΆ) β (((π½CnExtπΎ)βπΉ)βπ) = βͺ ((πΎ fLimf (((neiβπ½)β{π}) βΎt π΄))βπΉ)) | ||
Theorem | cnextf 23569* | Extension by continuity. The extension by continuity is a function. (Contributed by Thierry Arnoux, 25-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) β β’ (π β ((π½CnExtπΎ)βπΉ):πΆβΆπ΅) | ||
Theorem | cnextcn 23570* | Extension by continuity. Theorem 1 of [BourbakiTop1] p. I.57. Given a topology π½ on πΆ, a subset π΄ dense in πΆ, this states a condition for πΉ from π΄ to a regular space πΎ to be extensible by continuity. (Contributed by Thierry Arnoux, 1-Jan-2018.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) & β’ (π β πΎ β Reg) β β’ (π β ((π½CnExtπΎ)βπΉ) β (π½ Cn πΎ)) | ||
Theorem | cnextfres1 23571* | πΉ and its extension by continuity agree on the domain of πΉ. (Contributed by Thierry Arnoux, 17-Jan-2018.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β πΉ:π΄βΆπ΅) & β’ (π β π΄ β πΆ) & β’ (π β ((clsβπ½)βπ΄) = πΆ) & β’ ((π β§ π₯ β πΆ) β ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ) β β ) & β’ (π β πΎ β Reg) & β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) β β’ (π β (((π½CnExtπΎ)βπΉ) βΎ π΄) = πΉ) | ||
Theorem | cnextfres 23572 | πΉ and its extension by continuity agree on the domain of πΉ. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β π΄ β πΆ) & β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) & β’ (π β π β π΄) β β’ (π β (((π½CnExtπΎ)βπΉ)βπ) = (πΉβπ)) | ||
Syntax | ctmd 23573 | Extend class notation with the class of all topological monoids. |
class TopMnd | ||
Syntax | ctgp 23574 | Extend class notation with the class of all topological groups. |
class TopGrp | ||
Definition | df-tmd 23575* | Define the class of all topological monoids. A topological monoid is a monoid whose operation is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ TopMnd = {π β (Mnd β© TopSp) β£ [(TopOpenβπ) / π](+πβπ) β ((π Γt π) Cn π)} | ||
Definition | df-tgp 23576* | Define the class of all topological groups. A topological group is a group whose operation and inverse function are continuous. (Contributed by FL, 18-Apr-2010.) |
β’ TopGrp = {π β (Grp β© TopMnd) β£ [(TopOpenβπ) / π](invgβπ) β (π Cn π)} | ||
Theorem | istmd 23577 | The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ πΉ = (+πβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopMnd β (πΊ β Mnd β§ πΊ β TopSp β§ πΉ β ((π½ Γt π½) Cn π½))) | ||
Theorem | tmdmnd 23578 | A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (πΊ β TopMnd β πΊ β Mnd) | ||
Theorem | tmdtps 23579 | A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (πΊ β TopMnd β πΊ β TopSp) | ||
Theorem | istgp 23580 | The predicate "is a topological group". Definition 1 of [BourbakiTop1] p. III.1. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ πΌ = (invgβπΊ) β β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopMnd β§ πΌ β (π½ Cn π½))) | ||
Theorem | tgpgrp 23581 | A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ (πΊ β TopGrp β πΊ β Grp) | ||
Theorem | tgptmd 23582 | A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (πΊ β TopGrp β πΊ β TopMnd) | ||
Theorem | tgptps 23583 | A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ (πΊ β TopGrp β πΊ β TopSp) | ||
Theorem | tmdtopon 23584 | The topology of a topological monoid. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ π = (BaseβπΊ) β β’ (πΊ β TopMnd β π½ β (TopOnβπ)) | ||
Theorem | tgptopon 23585 | The topology of a topological group. (Contributed by Mario Carneiro, 27-Jun-2014.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ π = (BaseβπΊ) β β’ (πΊ β TopGrp β π½ β (TopOnβπ)) | ||
Theorem | tmdcn 23586 | In a topological monoid, the operation πΉ representing the functionalization of the operator slot +g is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ πΉ = (+πβπΊ) β β’ (πΊ β TopMnd β πΉ β ((π½ Γt π½) Cn π½)) | ||
Theorem | tgpcn 23587 | In a topological group, the operation πΉ representing the functionalization of the operator slot +g is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ πΉ = (+πβπΊ) β β’ (πΊ β TopGrp β πΉ β ((π½ Γt π½) Cn π½)) | ||
Theorem | tgpinv 23588 | In a topological group, the inverse function is continuous. (Contributed by FL, 21-Jun-2010.) (Revised by FL, 27-Jun-2014.) |
β’ π½ = (TopOpenβπΊ) & β’ πΌ = (invgβπΊ) β β’ (πΊ β TopGrp β πΌ β (π½ Cn π½)) | ||
Theorem | grpinvhmeo 23589 | The inverse function in a topological group is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ πΌ = (invgβπΊ) β β’ (πΊ β TopGrp β πΌ β (π½Homeoπ½)) | ||
Theorem | cnmpt1plusg 23590* | Continuity of the group sum; analogue of cnmpt12f 23169 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β TopMnd) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn π½)) & β’ (π β (π₯ β π β¦ π΅) β (πΎ Cn π½)) β β’ (π β (π₯ β π β¦ (π΄ + π΅)) β (πΎ Cn π½)) | ||
Theorem | cnmpt2plusg 23591* | Continuity of the group sum; analogue of cnmpt22f 23178 which cannot be used directly because +g is not a function. (Contributed by Mario Carneiro, 23-Aug-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ + = (+gβπΊ) & β’ (π β πΊ β TopMnd) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt πΏ) Cn π½)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((πΎ Γt πΏ) Cn π½)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄ + π΅)) β ((πΎ Γt πΏ) Cn π½)) | ||
Theorem | tmdcn2 23592* | Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ + = (+gβπΊ) β β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β βπ’ β π½ βπ£ β π½ (π β π’ β§ π β π£ β§ βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π)) | ||
Theorem | tgpsubcn 23593 | In a topological group, the "subtraction" (or "division") is continuous. Axiom GT' of [BourbakiTop1] p. III.1. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 19-Mar-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ β = (-gβπΊ) β β’ (πΊ β TopGrp β β β ((π½ Γt π½) Cn π½)) | ||
Theorem | istgp2 23594 | A group with a topology is a topological group iff the subtraction operation is continuous. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ β = (-gβπΊ) β β’ (πΊ β TopGrp β (πΊ β Grp β§ πΊ β TopSp β§ β β ((π½ Γt π½) Cn π½))) | ||
Theorem | tmdmulg 23595* | In a topological monoid, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ Β· = (.gβπΊ) & β’ π΅ = (BaseβπΊ) β β’ ((πΊ β TopMnd β§ π β β0) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) | ||
Theorem | tgpmulg 23596* | In a topological group, the n-times group multiple function is continuous. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ Β· = (.gβπΊ) & β’ π΅ = (BaseβπΊ) β β’ ((πΊ β TopGrp β§ π β β€) β (π₯ β π΅ β¦ (π Β· π₯)) β (π½ Cn π½)) | ||
Theorem | tgpmulg2 23597 | In a topological monoid, the group multiple function is jointly continuous (although this is not saying much as one of the factors is discrete). Use zdis 24331 to write the left topology as a subset of the complex numbers. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ Β· = (.gβπΊ) β β’ (πΊ β TopGrp β Β· β ((π« β€ Γt π½) Cn π½)) | ||
Theorem | tmdgsum 23598* | In a topological monoid, the group sum operation is a continuous function from the function space to the base topology. This theorem is not true when π΄ is infinite, because in this case for any basic open set of the domain one of the factors will be the whole space, so by varying the value of the functions to sum at this index, one can achieve any desired sum. (Contributed by Mario Carneiro, 19-Sep-2015.) (Proof shortened by AV, 24-Jul-2019.) |
β’ π½ = (TopOpenβπΊ) & β’ π΅ = (BaseβπΊ) β β’ ((πΊ β CMnd β§ πΊ β TopMnd β§ π΄ β Fin) β (π₯ β (π΅ βm π΄) β¦ (πΊ Ξ£g π₯)) β ((π½ βko π« π΄) Cn π½)) | ||
Theorem | tmdgsum2 23599* | For any neighborhood π of ππ, there is a neighborhood π’ of π such that any sum of π elements in π’ sums to an element of π. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ π΅ = (BaseβπΊ) & β’ Β· = (.gβπΊ) & β’ (π β πΊ β CMnd) & β’ (π β πΊ β TopMnd) & β’ (π β π΄ β Fin) & β’ (π β π β π½) & β’ (π β π β π΅) & β’ (π β ((β―βπ΄) Β· π) β π) β β’ (π β βπ’ β π½ (π β π’ β§ βπ β (π’ βm π΄)(πΊ Ξ£g π) β π)) | ||
Theorem | oppgtmd 23600 | The opposite of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π = (oppgβπΊ) β β’ (πΊ β TopMnd β π β TopMnd) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |