Home | Metamath
Proof Explorer Theorem List (p. 234 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | flimfnfcls 23301* | A filter converges to a point iff every finer filter clusters there. Along with fclsfnflim 23300, 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 23302 | Forward direction of fclscmp 23303. 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 23303* | 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 23304 | 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 23305* | 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 23306 | 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 23307* | 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 23308* | 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 23309 | 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 23310 | 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 23311 | 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 23312 | 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 23313 | Lemma for cnpfcf 23314. 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 23314* | 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 23315* | 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 23316 | 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 23317* | Lemma for alexsub 23318. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ (π β π β UFL) & β’ (π β π = βͺ π΅) & β’ (π β π½ = (topGenβ(fiβπ΅))) & β’ ((π β§ (π₯ β π΅ β§ π = βͺ π₯)) β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦) & β’ (π β πΉ β (UFilβπ)) & β’ (π β (π½ fLim πΉ) = β ) β β’ Β¬ π | ||
Theorem | alexsub 23318* | 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 23324 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 23319* | Biconditional form of the Alexander Subbase Theorem alexsub 23318. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ ((π β UFL β§ π = βͺ π΅) β ((topGenβ(fiβπ΅)) β Comp β βπ₯ β π« π΅(π = βͺ π₯ β βπ¦ β (π« π₯ β© Fin)π = βͺ π¦))) | ||
Theorem | alexsubALTlem1 23320* | Lemma for alexsubALT 23324. 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 23321* | Lemma for alexsubALT 23324. 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 23322* | Lemma for alexsubALT 23324. 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 23323* | Lemma for alexsubALT 23324. 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 23324* | 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 23325* | Lemma for ptcmp 23331. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) β β’ (π β (π = βͺ (ran π βͺ {π}) β§ (βtβπΉ) = (topGenβ(fiβ(ran π βͺ {π}))))) | ||
Theorem | ptcmplem2 23326* | Lemma for ptcmp 23331. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) β β’ (π β βͺ π β {π β π΄ β£ Β¬ βͺ (πΉβπ) β 1o}βͺ (πΉβπ) β dom card) | ||
Theorem | ptcmplem3 23327* | Lemma for ptcmp 23331. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) & β’ πΎ = {π’ β (πΉβπ) β£ (β‘(π€ β π β¦ (π€βπ)) β π’) β π} β β’ (π β βπ(π Fn π΄ β§ βπ β π΄ (πβπ) β (βͺ (πΉβπ) β βͺ πΎ))) | ||
Theorem | ptcmplem4 23328* | Lemma for ptcmp 23331. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) & β’ (π β π β ran π) & β’ (π β π = βͺ π) & β’ (π β Β¬ βπ§ β (π« π β© Fin)π = βͺ π§) & β’ πΎ = {π’ β (πΉβπ) β£ (β‘(π€ β π β¦ (π€βπ)) β π’) β π} β β’ Β¬ π | ||
Theorem | ptcmplem5 23329* | Lemma for ptcmp 23331. (Contributed by Mario Carneiro, 26-Aug-2015.) |
β’ π = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) & β’ π = Xπ β π΄ βͺ (πΉβπ) & β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆComp) & β’ (π β π β (UFL β© dom card)) β β’ (π β (βtβπΉ) β Comp) | ||
Theorem | ptcmpg 23330 | 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 23331). (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π½ = (βtβπΉ) & β’ π = βͺ π½ β β’ ((π΄ β π β§ πΉ:π΄βΆComp β§ π β (UFL β© dom card)) β π½ β Comp) | ||
Theorem | ptcmp 23331 | 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 23332 | Extend class notation with the continuous extension operation. |
class CnExt | ||
Definition | df-cnext 23333* | 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 23334* | 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 23335* | The continuous extension of a given function πΉ. (Contributed by Thierry Arnoux, 1-Dec-2017.) |
β’ π = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β π)) β ((π½CnExtπΎ)βπΉ) = βͺ π₯ β ((clsβπ½)βπ΄)({π₯} Γ ((πΎ fLimf (((neiβπ½)β{π₯}) βΎt π΄))βπΉ))) | ||
Theorem | cnextrel 23336 | In the general case, a continuous extension is a relation. (Contributed by Thierry Arnoux, 20-Dec-2017.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (πΉ:π΄βΆπ΅ β§ π΄ β πΆ)) β Rel ((π½CnExtπΎ)βπΉ)) | ||
Theorem | cnextfun 23337 | 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 23338* | 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 23339* | 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 23340* | 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 23341* | πΉ 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 23342 | πΉ and its extension by continuity agree on the domain of πΉ. (Contributed by Thierry Arnoux, 29-Aug-2020.) |
β’ πΆ = βͺ π½ & β’ π΅ = βͺ πΎ & β’ (π β π½ β Top) & β’ (π β πΎ β Haus) & β’ (π β π΄ β πΆ) & β’ (π β πΉ β ((π½ βΎt π΄) Cn πΎ)) & β’ (π β π β π΄) β β’ (π β (((π½CnExtπΎ)βπΉ)βπ) = (πΉβπ)) | ||
Syntax | ctmd 23343 | Extend class notation with the class of all topological monoids. |
class TopMnd | ||
Syntax | ctgp 23344 | Extend class notation with the class of all topological groups. |
class TopGrp | ||
Definition | df-tmd 23345* | 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 23346* | 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 23347 | The predicate "is a topological monoid". (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ πΉ = (+πβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopMnd β (πΊ β Mnd β§ πΊ β TopSp β§ πΉ β ((π½ Γt π½) Cn π½))) | ||
Theorem | tmdmnd 23348 | A topological monoid is a monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (πΊ β TopMnd β πΊ β Mnd) | ||
Theorem | tmdtps 23349 | A topological monoid is a topological space. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (πΊ β TopMnd β πΊ β TopSp) | ||
Theorem | istgp 23350 | 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 23351 | A topological group is a group. (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ (πΊ β TopGrp β πΊ β Grp) | ||
Theorem | tgptmd 23352 | A topological group is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (πΊ β TopGrp β πΊ β TopMnd) | ||
Theorem | tgptps 23353 | A topological group is a topological space. (Contributed by FL, 21-Jun-2010.) (Revised by Mario Carneiro, 13-Aug-2015.) |
β’ (πΊ β TopGrp β πΊ β TopSp) | ||
Theorem | tmdtopon 23354 | 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 23355 | 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 23356 | 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 23357 | 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 23358 | 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 23359 | 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 23360* | Continuity of the group sum; analogue of cnmpt12f 22939 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 23361* | Continuity of the group sum; analogue of cnmpt22f 22948 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 23362* | Write out the definition of continuity of +g explicitly. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ + = (+gβπΊ) β β’ (((πΊ β TopMnd β§ π β π½) β§ (π β π΅ β§ π β π΅ β§ (π + π) β π)) β βπ’ β π½ βπ£ β π½ (π β π’ β§ π β π£ β§ βπ₯ β π’ βπ¦ β π£ (π₯ + π¦) β π)) | ||
Theorem | tgpsubcn 23363 | 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 23364 | 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 23365* | 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 23366* | 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 23367 | 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 24101 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 23368* | 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 23369* | 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 23370 | The opposite of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π = (oppgβπΊ) β β’ (πΊ β TopMnd β π β TopMnd) | ||
Theorem | oppgtgp 23371 | The opposite of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (oppgβπΊ) β β’ (πΊ β TopGrp β π β TopGrp) | ||
Theorem | distgp 23372 | Any group equipped with the discrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β Grp β§ π½ = π« π΅) β πΊ β TopGrp) | ||
Theorem | indistgp 23373 | Any group equipped with the indiscrete topology is a topological group. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ π΅ = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β Grp β§ π½ = {β , π΅}) β πΊ β TopGrp) | ||
Theorem | efmndtmd 23374 | The monoid of endofunctions on a set π΄ is a topological monoid. Formerly part of proof for symgtgp 23379. (Contributed by AV, 23-Feb-2024.) |
β’ π = (EndoFMndβπ΄) β β’ (π΄ β π β π β TopMnd) | ||
Theorem | tmdlactcn 23375* | The left group action of element π΄ in a topological monoid πΊ is a continuous function. (Contributed by FL, 18-Mar-2008.) (Revised by Mario Carneiro, 14-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ (π΄ + π₯)) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopMnd β§ π΄ β π) β πΉ β (π½ Cn π½)) | ||
Theorem | tgplacthmeo 23376* | The left group action of element π΄ in a topological group πΊ is a homeomorphism from the group to itself. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ (π΄ + π₯)) & β’ π = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π΄ β π) β πΉ β (π½Homeoπ½)) | ||
Theorem | submtmd 23377 | A submonoid of a topological monoid is a topological monoid. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β TopMnd β§ π β (SubMndβπΊ)) β π» β TopMnd) | ||
Theorem | subgtgp 23378 | A subgroup of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π» = (πΊ βΎs π) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β π» β TopGrp) | ||
Theorem | symgtgp 23379 | The symmetric group is a topological group. (Contributed by Mario Carneiro, 2-Sep-2015.) (Proof shortened by AV, 30-Mar-2024.) |
β’ πΊ = (SymGrpβπ΄) β β’ (π΄ β π β πΊ β TopGrp) | ||
Theorem | subgntr 23380 | A subgroup of a topological group with nonempty interior is open. Alternatively, dual to clssubg 23382, the interior of a subgroup is either a subgroup, or empty. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π΄ β ((intβπ½)βπ)) β π β π½) | ||
Theorem | opnsubg 23381 | An open subgroup of a topological group is also closed. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π β π½) β π β (Clsdβπ½)) | ||
Theorem | clssubg 23382 | The closure of a subgroup in a topological group is a subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ)) β ((clsβπ½)βπ) β (SubGrpβπΊ)) | ||
Theorem | clsnsg 23383 | The closure of a normal subgroup is a normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β ((clsβπ½)βπ) β (NrmSGrpβπΊ)) | ||
Theorem | cldsubg 23384 | A subgroup of finite index is closed iff it is open. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) & β’ π = (πΊ ~QG π) & β’ π = (BaseβπΊ) β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ (π / π ) β Fin) β (π β (Clsdβπ½) β π β π½)) | ||
Theorem | tgpconncompeqg 23385* | The connected component containing π΄ is the left coset of the identity component containing π΄. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = βͺ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} & β’ βΌ = (πΊ ~QG π) β β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ = βͺ {π₯ β π« π β£ (π΄ β π₯ β§ (π½ βΎt π₯) β Conn)}) | ||
Theorem | tgpconncomp 23386* | The identity component, the connected component containing the identity element, is a closed (conncompcld 22707) normal subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = βͺ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ (πΊ β TopGrp β π β (NrmSGrpβπΊ)) | ||
Theorem | tgpconncompss 23387* | The identity component is a subset of any open subgroup. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ π = βͺ {π₯ β π« π β£ ( 0 β π₯ β§ (π½ βΎt π₯) β Conn)} β β’ ((πΊ β TopGrp β§ π β (SubGrpβπΊ) β§ π β π½) β π β π) | ||
Theorem | ghmcnp 23388 | A group homomorphism on topological groups is continuous everywhere if it is continuous at any point. (Contributed by Mario Carneiro, 21-Oct-2015.) |
β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») β β’ ((πΊ β TopMnd β§ π» β TopMnd β§ πΉ β (πΊ GrpHom π»)) β (πΉ β ((π½ CnP πΎ)βπ΄) β (π΄ β π β§ πΉ β (π½ Cn πΎ)))) | ||
Theorem | snclseqg 23389 | The coset of the closure of the identity is the closure of a point. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ 0 = (0gβπΊ) & β’ βΌ = (πΊ ~QG π) & β’ π = ((clsβπ½)β{ 0 }) β β’ ((πΊ β TopGrp β§ π΄ β π) β [π΄] βΌ = ((clsβπ½)β{π΄})) | ||
Theorem | tgphaus 23390 | A topological group is Hausdorff iff the identity subgroup is closed. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ 0 = (0gβπΊ) & β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopGrp β (π½ β Haus β { 0 } β (Clsdβπ½))) | ||
Theorem | tgpt1 23391 | Hausdorff and T1 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopGrp β (π½ β Haus β π½ β Fre)) | ||
Theorem | tgpt0 23392 | Hausdorff and T0 are equivalent for topological groups. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π½ = (TopOpenβπΊ) β β’ (πΊ β TopGrp β (π½ β Haus β π½ β Kol2)) | ||
Theorem | qustgpopn 23393* | A quotient map in a topological group is an open map. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») & β’ πΉ = (π₯ β π β¦ [π₯](πΊ ~QG π)) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β π½) β (πΉ β π) β πΎ) | ||
Theorem | qustgplem 23394* | Lemma for qustgp 23395. (Contributed by Mario Carneiro, 18-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π = (BaseβπΊ) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») & β’ πΉ = (π₯ β π β¦ [π₯](πΊ ~QG π)) & β’ β = (π§ β π, π€ β π β¦ [(π§(-gβπΊ)π€)](πΊ ~QG π)) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β π» β TopGrp) | ||
Theorem | qustgp 23395 | The quotient of a topological group is a topological group. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ)) β π» β TopGrp) | ||
Theorem | qustgphaus 23396 | The quotient of a topological group by a closed normal subgroup is a Hausdorff topological group. In particular, the quotient by the closure of the identity is a Hausdorff topological group, isomorphic to both the Kolmogorov quotient and the Hausdorff quotient operations on topological spaces (because T0 and Hausdorff coincide for topological groups). (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π» = (πΊ /s (πΊ ~QG π)) & β’ π½ = (TopOpenβπΊ) & β’ πΎ = (TopOpenβπ») β β’ ((πΊ β TopGrp β§ π β (NrmSGrpβπΊ) β§ π β (Clsdβπ½)) β πΎ β Haus) | ||
Theorem | prdstmdd 23397 | The product of a family of topological monoids is a topological monoid. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆTopMnd) β β’ (π β π β TopMnd) | ||
Theorem | prdstgpd 23398 | The product of a family of topological groups is a topological group. (Contributed by Mario Carneiro, 22-Sep-2015.) |
β’ π = (πXsπ ) & β’ (π β πΌ β π) & β’ (π β π β π) & β’ (π β π :πΌβΆTopGrp) β β’ (π β π β TopGrp) | ||
Syntax | ctsu 23399 | Extend class notation to include infinite group sums in a topological group. |
class tsums | ||
Definition | df-tsms 23400* | Define the set of limit points of an infinite group sum for the topological group πΊ. If πΊ is Hausdorff, then there will be at most one element in this set and βͺ (π tsums πΉ) selects this unique element if it exists. (π tsums πΉ) β 1o is a way to say that the sum exists and is unique. Note that unlike Ξ£ (df-sum 15506) and Ξ£g (df-gsum 17259), this does not return the sum itself, but rather the set of all such sums, which is usually either empty or a singleton. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ tsums = (π€ β V, π β V β¦ β¦(π« dom π β© Fin) / π β¦(((TopOpenβπ€) fLimf (π filGenran (π§ β π β¦ {π¦ β π β£ π§ β π¦})))β(π¦ β π β¦ (π€ Ξ£g (π βΎ π¦))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |