Home | Metamath
Proof Explorer Theorem List (p. 230 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 | prdstopn 22901 | Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ π = (TopOpenβπ) β β’ (π β π = (βtβ(TopOpen β π ))) | ||
Theorem | prdstps 22902 | A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆTopSp) β β’ (π β π β TopSp) | ||
Theorem | pwstps 22903 | A structure power of a topological space is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β TopSp β§ πΌ β π) β π β TopSp) | ||
Theorem | txrest 22904 | The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 2-Sep-2015.) |
β’ (((π β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β ((π Γt π) βΎt (π΄ Γ π΅)) = ((π βΎt π΄) Γt (π βΎt π΅))) | ||
Theorem | txdis 22905 | The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (π« π΄ Γt π« π΅) = π« (π΄ Γ π΅)) | ||
Theorem | txindislem 22906 | Lemma for txindis 22907. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (( I βπ΄) Γ ( I βπ΅)) = ( I β(π΄ Γ π΅)) | ||
Theorem | txindis 22907 | The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ({β , π΄} Γt {β , π΅}) = {β , (π΄ Γ π΅)} | ||
Theorem | txdis1cn 22908* | A function is jointly continuous on a discrete left topology iff it is continuous as a function of its right argument, for each fixed left value. (Contributed by Mario Carneiro, 19-Sep-2015.) |
β’ (π β π β π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β Top) & β’ (π β πΉ Fn (π Γ π)) & β’ ((π β§ π₯ β π) β (π¦ β π β¦ (π₯πΉπ¦)) β (π½ Cn πΎ)) β β’ (π β πΉ β ((π« π Γt π½) Cn πΎ)) | ||
Theorem | txlly 22909* | If the property π΄ is preserved under topological products, then so is the property of being locally π΄. (Contributed by Mario Carneiro, 10-Mar-2015.) |
β’ ((π β π΄ β§ π β π΄) β (π Γt π) β π΄) β β’ ((π β Locally π΄ β§ π β Locally π΄) β (π Γt π) β Locally π΄) | ||
Theorem | txnlly 22910* | If the property π΄ is preserved under topological products, then so is the property of being n-locally π΄. (Contributed by Mario Carneiro, 13-Apr-2015.) |
β’ ((π β π΄ β§ π β π΄) β (π Γt π) β π΄) β β’ ((π β π-Locally π΄ β§ π β π-Locally π΄) β (π Γt π) β π-Locally π΄) | ||
Theorem | pthaus 22911 | The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆHaus) β (βtβπΉ) β Haus) | ||
Theorem | ptrescn 22912* | Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ π = βͺ π½ & β’ π½ = (βtβπΉ) & β’ πΎ = (βtβ(πΉ βΎ π΅)) β β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (π₯ β π β¦ (π₯ βΎ π΅)) β (π½ Cn πΎ)) | ||
Theorem | txtube 22913* | The "tube lemma". If π is compact and there is an open set π containing the line π Γ {π΄}, then there is a "tube" π Γ π’ for some neighborhood π’ of π΄ which is entirely contained within π. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ π = βͺ π & β’ π = βͺ π & β’ (π β π β Comp) & β’ (π β π β Top) & β’ (π β π β (π Γt π)) & β’ (π β (π Γ {π΄}) β π) & β’ (π β π΄ β π) β β’ (π β βπ’ β π (π΄ β π’ β§ (π Γ π’) β π)) | ||
Theorem | txcmplem1 22914* | Lemma for txcmp 22916. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π & β’ π = βͺ π & β’ (π β π β Comp) & β’ (π β π β Comp) & β’ (π β π β (π Γt π)) & β’ (π β (π Γ π) = βͺ π) & β’ (π β π΄ β π) β β’ (π β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) | ||
Theorem | txcmplem2 22915* | Lemma for txcmp 22916. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π & β’ π = βͺ π & β’ (π β π β Comp) & β’ (π β π β Comp) & β’ (π β π β (π Γt π)) & β’ (π β (π Γ π) = βͺ π) β β’ (π β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£) | ||
Theorem | txcmp 22916 | The topological product of two compact spaces is compact. (Contributed by Mario Carneiro, 14-Sep-2014.) (Proof shortened 21-Mar-2015.) |
β’ ((π β Comp β§ π β Comp) β (π Γt π) β Comp) | ||
Theorem | txcmpb 22917 | The topological product of two nonempty topologies is compact iff the component topologies are both compact. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π & β’ π = βͺ π β β’ (((π β Top β§ π β Top) β§ (π β β β§ π β β )) β ((π Γt π) β Comp β (π β Comp β§ π β Comp))) | ||
Theorem | hausdiag 22918 | A topology is Hausdorff iff the diagonal set is closed in the topology's product with itself. EDITORIAL: very clumsy proof, can probably be shortened substantially. (Contributed by Stefan O'Rear, 25-Jan-2015.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) |
β’ π = βͺ π½ β β’ (π½ β Haus β (π½ β Top β§ ( I βΎ π) β (Clsdβ(π½ Γt π½)))) | ||
Theorem | hauseqlcld 22919 | In a Hausdorff topology, the equalizer of two continuous functions is closed (thus, two continuous functions which agree on a dense set agree everywhere). (Contributed by Stefan O'Rear, 25-Jan-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β πΎ β Haus) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β πΊ β (π½ Cn πΎ)) β β’ (π β dom (πΉ β© πΊ) β (Clsdβπ½)) | ||
Theorem | txhaus 22920 | The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π β Haus β§ π β Haus) β (π Γt π) β Haus) | ||
Theorem | txlm 22921* | Two sequences converge iff the sequence of their ordered pairs converges. Proposition 14-2.6 of [Gleason] p. 230. (Contributed by NM, 16-Jul-2007.) (Revised by Mario Carneiro, 5-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) & β’ π» = (π β π β¦ β¨(πΉβπ), (πΊβπ)β©) β β’ (π β ((πΉ(βπ‘βπ½)π β§ πΊ(βπ‘βπΎ)π) β π»(βπ‘β(π½ Γt πΎ))β¨π , πβ©)) | ||
Theorem | lmcn2 22922* | 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, 15-May-2014.) |
β’ π = (β€β₯βπ) & β’ (π β π β β€) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ:πβΆπ) & β’ (π β πΊ:πβΆπ) & β’ (π β πΉ(βπ‘βπ½)π ) & β’ (π β πΊ(βπ‘βπΎ)π) & β’ (π β π β ((π½ Γt πΎ) Cn π)) & β’ π» = (π β π β¦ ((πΉβπ)π(πΊβπ))) β β’ (π β π»(βπ‘βπ)(π ππ)) | ||
Theorem | tx1stc 22923 | The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π β 1stΟ β§ π β 1stΟ) β (π Γt π) β 1stΟ) | ||
Theorem | tx2ndc 22924 | The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π β 2ndΟ β§ π β 2ndΟ) β (π Γt π) β 2ndΟ) | ||
Theorem | txkgen 22925 | The topological product of a locally compact space and a compactly generated Hausdorff space is compactly generated. (The condition on π can also be replaced with either "compactly generated weak Hausdorff (CGWH)" or "compact Hausdorff-ly generated (CHG)", where WH means that all images of compact Hausdorff spaces are closed and CHG means that a set is open iff it is open in all compact Hausdorff spaces.) (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π β π-Locally Comp β§ π β (ran πGen β© Haus)) β (π Γt π) β ran πGen) | ||
Theorem | xkohaus 22926 | If the codomain space is Hausdorff, then the compact-open topology of continuous functions is also Hausdorff. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π β Top β§ π β Haus) β (π βko π ) β Haus) | ||
Theorem | xkoptsub 22927 | The compact-open topology is finer than the product topology restricted to continuous functions. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π & β’ π½ = (βtβ(π Γ {π})) β β’ ((π β Top β§ π β Top) β (π½ βΎt (π Cn π)) β (π βko π )) | ||
Theorem | xkopt 22928 | The compact-open topology on a discrete set coincides with the product topology where all the factors are the same. (Contributed by Mario Carneiro, 19-Mar-2015.) (Revised by Mario Carneiro, 12-Sep-2015.) |
β’ ((π β Top β§ π΄ β π) β (π βko π« π΄) = (βtβ(π΄ Γ {π }))) | ||
Theorem | xkopjcn 22929* | Continuity of a projection map from the space of continuous functions. (This theorem can be strengthened, to joint continuity in both π and π΄ as a function on (π βko π ) Γt π , but not without stronger assumptions on π ; see xkofvcn 22957.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π β β’ ((π β Top β§ π β Top β§ π΄ β π) β (π β (π Cn π) β¦ (πβπ΄)) β ((π βko π ) Cn π)) | ||
Theorem | xkoco1cn 22930* | If πΉ is a continuous function, then π β¦ π β πΉ is a continuous function on function spaces. (The reason we prove this and xkoco2cn 22931 independently of the more general xkococn 22933 is because that requires some inconvenient extra assumptions on π.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β Top) & β’ (π β πΉ β (π Cn π)) β β’ (π β (π β (π Cn π) β¦ (π β πΉ)) β ((π βko π) Cn (π βko π ))) | ||
Theorem | xkoco2cn 22931* | If πΉ is a continuous function, then π β¦ πΉ β π is a continuous function on function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (π β π β Top) & β’ (π β πΉ β (π Cn π)) β β’ (π β (π β (π Cn π) β¦ (πΉ β π)) β ((π βko π ) Cn (π βko π ))) | ||
Theorem | xkococnlem 22932* | Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ πΉ = (π β (π Cn π), π β (π Cn π) β¦ (π β π)) & β’ (π β π β π-Locally Comp) & β’ (π β πΎ β βͺ π ) & β’ (π β (π βΎt πΎ) β Comp) & β’ (π β π β π) & β’ (π β π΄ β (π Cn π)) & β’ (π β π΅ β (π Cn π)) & β’ (π β ((π΄ β π΅) β πΎ) β π) β β’ (π β βπ§ β ((π βko π) Γt (π βko π ))(β¨π΄, π΅β© β π§ β§ π§ β (β‘πΉ β {β β (π Cn π) β£ (β β πΎ) β π}))) | ||
Theorem | xkococn 22933* | Continuity of the composition operation as a function on continuous function spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ πΉ = (π β (π Cn π), π β (π Cn π) β¦ (π β π)) β β’ ((π β Top β§ π β π-Locally Comp β§ π β Top) β πΉ β (((π βko π) Γt (π βko π )) Cn (π βko π ))) | ||
Theorem | cnmptid 22934* | The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) β β’ (π β (π₯ β π β¦ π₯) β (π½ Cn π½)) | ||
Theorem | cnmptc 22935* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (π₯ β π β¦ π) β (π½ Cn πΎ)) | ||
Theorem | cnmpt11 22936* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π¦ β π β¦ π΅) β (πΎ Cn πΏ)) & β’ (π¦ = π΄ β π΅ = πΆ) β β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) | ||
Theorem | cnmpt11f 22937* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) & β’ (π β πΉ β (πΎ Cn πΏ)) β β’ (π β (π₯ β π β¦ (πΉβπ΄)) β (π½ Cn πΏ)) | ||
Theorem | cnmpt1t 22938* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) & β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΏ)) β β’ (π β (π₯ β π β¦ β¨π΄, π΅β©) β (π½ Cn (πΎ Γt πΏ))) | ||
Theorem | cnmpt12f 22939* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) & β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΏ)) & β’ (π β πΉ β ((πΎ Γt πΏ) Cn π)) β β’ (π β (π₯ β π β¦ (π΄πΉπ΅)) β (π½ Cn π)) | ||
Theorem | cnmpt12 22940* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 12-Jun-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΎ)) & β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΏ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π¦ β π, π§ β π β¦ πΆ) β ((πΎ Γt πΏ) Cn π)) & β’ ((π¦ = π΄ β§ π§ = π΅) β πΆ = π·) β β’ (π β (π₯ β π β¦ π·) β (π½ Cn π)) | ||
Theorem | cnmpt1st 22941* | The projection onto the first coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) β β’ (π β (π₯ β π, π¦ β π β¦ π₯) β ((π½ Γt πΎ) Cn π½)) | ||
Theorem | cnmpt2nd 22942* | The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) β β’ (π β (π₯ β π, π¦ β π β¦ π¦) β ((π½ Γt πΎ) Cn πΎ)) | ||
Theorem | cnmpt2c 22943* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (π₯ β π, π¦ β π β¦ π) β ((π½ Γt πΎ) Cn πΏ)) | ||
Theorem | cnmpt21 22944* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π§ β π β¦ π΅) β (πΏ Cn π)) & β’ (π§ = π΄ β π΅ = πΆ) β β’ (π β (π₯ β π, π¦ β π β¦ πΆ) β ((π½ Γt πΎ) Cn π)) | ||
Theorem | cnmpt21f 22945* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) & β’ (π β πΉ β (πΏ Cn π)) β β’ (π β (π₯ β π, π¦ β π β¦ (πΉβπ΄)) β ((π½ Γt πΎ) Cn π)) | ||
Theorem | cnmpt2t 22946* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΎ) Cn π)) β β’ (π β (π₯ β π, π¦ β π β¦ β¨π΄, π΅β©) β ((π½ Γt πΎ) Cn (πΏ Γt π))) | ||
Theorem | cnmpt22 22947* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΎ) Cn π)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ (π β (π§ β π, π€ β π β¦ πΆ) β ((πΏ Γt π) Cn π)) & β’ ((π§ = π΄ β§ π€ = π΅) β πΆ = π·) β β’ (π β (π₯ β π, π¦ β π β¦ π·) β ((π½ Γt πΎ) Cn π)) | ||
Theorem | cnmpt22f 22948* | The composition of continuous functions is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΅) β ((π½ Γt πΎ) Cn π)) & β’ (π β πΉ β ((πΏ Γt π) Cn π)) β β’ (π β (π₯ β π, π¦ β π β¦ (π΄πΉπ΅)) β ((π½ Γt πΎ) Cn π)) | ||
Theorem | cnmpt1res 22949* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.) |
β’ πΎ = (π½ βΎt π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΏ)) β β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn πΏ)) | ||
Theorem | cnmpt2res 22950* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ πΎ = (π½ βΎt π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ π = (π βΎt π) & β’ (π β π β (TopOnβπ)) & β’ (π β π β π) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt π) Cn πΏ)) β β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((πΎ Γt π) Cn πΏ)) | ||
Theorem | cnmptcom 22951* | The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β β’ (π β (π¦ β π, π₯ β π β¦ π΄) β ((πΎ Γt π½) Cn πΏ)) | ||
Theorem | cnmptkc 22952* | The curried first projection function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ π₯)) β (π½ Cn (π½ βko πΎ))) | ||
Theorem | cnmptkp 22953* | The evaluation of the inner function in a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β π΅ β π) & β’ (π¦ = π΅ β π΄ = πΆ) β β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) | ||
Theorem | cnmptk1 22954* | The composition of a curried function with a one-arg function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β (π§ β π β¦ π΅) β (πΏ Cn π)) & β’ (π§ = π΄ β π΅ = πΆ) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ πΆ)) β (π½ Cn (π βko πΎ))) | ||
Theorem | cnmpt1k 22955* | The composition of a one-arg function with a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΏ)) & β’ (π β (π¦ β π β¦ (π§ β π β¦ π΅)) β (πΎ Cn (π βko πΏ))) & β’ (π§ = π΄ β π΅ = πΆ) β β’ (π β (π¦ β π β¦ (π₯ β π β¦ πΆ)) β (πΎ Cn (π βko π½))) | ||
Theorem | cnmptkk 22956* | The composition of two curried functions is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π β (TopOnβπ)) & β’ (π β πΏ β π-Locally Comp) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β (π₯ β π β¦ (π§ β π β¦ π΅)) β (π½ Cn (π βko πΏ))) & β’ (π§ = π΄ β π΅ = πΆ) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ πΆ)) β (π½ Cn (π βko πΎ))) | ||
Theorem | xkofvcn 22957* | Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 22929.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π & β’ πΉ = (π β (π Cn π), π₯ β π β¦ (πβπ₯)) β β’ ((π β π-Locally Comp β§ π β Top) β πΉ β (((π βko π ) Γt π ) Cn π)) | ||
Theorem | cnmptk1p 22958* | The evaluation of a curried function by a one-arg function is jointly continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β πΎ β π-Locally Comp) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) & β’ (π β (π₯ β π β¦ π΅) β (π½ Cn πΎ)) & β’ (π¦ = π΅ β π΄ = πΆ) β β’ (π β (π₯ β π β¦ πΆ) β (π½ Cn πΏ)) | ||
Theorem | cnmptk2 22959* | The uncurrying of a curried function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β πΎ β π-Locally Comp) & β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) β β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) | ||
Theorem | xkoinjcn 22960* | Continuity of "injection", i.e. currying, as a function on continuous function spaces. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ πΉ = (π₯ β π β¦ (π¦ β π β¦ β¨π¦, π₯β©)) β β’ ((π β (TopOnβπ) β§ π β (TopOnβπ)) β πΉ β (π Cn ((π Γt π ) βko π))) | ||
Theorem | cnmpt2k 22961* | The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) | ||
Theorem | txconn 22962 | The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.) |
β’ ((π β Conn β§ π β Conn) β (π Γt π) β Conn) | ||
Theorem | imasnopn 22963 | If a relation graph is open, then an image set of a singleton is also open. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ πΎ β Top) β§ (π β (π½ Γt πΎ) β§ π΄ β π)) β (π β {π΄}) β πΎ) | ||
Theorem | imasncld 22964 | If a relation graph is closed, then an image set of a singleton is also closed. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
β’ π = βͺ π½ β β’ (((π½ β Top β§ πΎ β Top) β§ (π β (Clsdβ(π½ Γt πΎ)) β§ π΄ β π)) β (π β {π΄}) β (ClsdβπΎ)) | ||
Theorem | imasncls 22965 | If a relation graph is closed, then an image set of a singleton is also closed. Corollary of Proposition 4 of [BourbakiTop1] p. I.26. (Contributed by Thierry Arnoux, 14-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (π β (π Γ π) β§ π΄ β π)) β ((clsβπΎ)β(π β {π΄})) β (((clsβ(π½ Γt πΎ))βπ ) β {π΄})) | ||
Syntax | ckq 22966 | Extend class notation with the Kolmogorov quotient function. |
class KQ | ||
Definition | df-kq 22967* | Define the Kolmogorov quotient. This is a function on topologies which maps a topology to its quotient under the topological distinguishability map, which takes a point to the set of open sets that contain it. Two points are mapped to the same image under this function iff they are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ KQ = (π β Top β¦ (π qTop (π₯ β βͺ π β¦ {π¦ β π β£ π₯ β π¦}))) | ||
Theorem | qtopval 22968* | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ β π) β (π½ qTop πΉ) = {π β π« (πΉ β π) β£ ((β‘πΉ β π ) β© π) β π½}) | ||
Theorem | qtopval2 22969* | Value of the quotient topology function when πΉ is a function on the base set. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ β§ π β π) β (π½ qTop πΉ) = {π β π« π β£ (β‘πΉ β π ) β π½}) | ||
Theorem | elqtop 22970 | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ β§ π β π) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtopres 22971 | The quotient topology is unaffected by restriction to the base set. This property makes it slightly more convenient to use, since we don't have to require that πΉ be a function with domain π. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ (πΉ β π β (π½ qTop πΉ) = (π½ qTop (πΉ βΎ π))) | ||
Theorem | qtoptop2 22972 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π½ qTop πΉ) β Top) | ||
Theorem | qtoptop 22973 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ Fn π) β (π½ qTop πΉ) β Top) | ||
Theorem | elqtop2 22974 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtopuni 22975 | The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ:πβontoβπ) β π = βͺ (π½ qTop πΉ)) | ||
Theorem | elqtop3 22976 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtoptopon 22977 | The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) | ||
Theorem | qtopid 22978 | A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ Fn π) β πΉ β (π½ Cn (π½ qTop πΉ))) | ||
Theorem | idqtop 22979 | The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ qTop ( I βΎ π)) = π½) | ||
Theorem | qtopcmplem 22980 | Lemma for qtopcmp 22981 and qtopconn 22982. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ & β’ (π½ β π΄ β π½ β Top) & β’ ((π½ β π΄ β§ πΉ:πβontoββͺ (π½ qTop πΉ) β§ πΉ β (π½ Cn (π½ qTop πΉ))) β (π½ qTop πΉ) β π΄) β β’ ((π½ β π΄ β§ πΉ Fn π) β (π½ qTop πΉ) β π΄) | ||
Theorem | qtopcmp 22981 | A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ πΉ Fn π) β (π½ qTop πΉ) β Comp) | ||
Theorem | qtopconn 22982 | A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Conn β§ πΉ Fn π) β (π½ qTop πΉ) β Conn) | ||
Theorem | qtopkgen 22983 | A quotient of a compactly generated space is compactly generated. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β ran πGen β§ πΉ Fn π) β (π½ qTop πΉ) β ran πGen) | ||
Theorem | basqtop 22984 | An injection maps bases to bases. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β TopBases β§ πΉ:πβ1-1-ontoβπ) β (π½ qTop πΉ) β TopBases) | ||
Theorem | tgqtop 22985 | An injection maps generated topologies to each other. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = βͺ π½ β β’ ((π½ β TopBases β§ πΉ:πβ1-1-ontoβπ) β ((topGenβπ½) qTop πΉ) = (topGenβ(π½ qTop πΉ))) | ||
Theorem | qtopcld 22986 | The property of being a closed set in the quotient topology. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β (Clsdβ(π½ qTop πΉ)) β (π΄ β π β§ (β‘πΉ β π΄) β (Clsdβπ½)))) | ||
Theorem | qtopcn 22987 | Universal property of a quotient map. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β§ (πΉ:πβontoβπ β§ πΊ:πβΆπ)) β (πΊ β ((π½ qTop πΉ) Cn πΎ) β (πΊ β πΉ) β (π½ Cn πΎ))) | ||
Theorem | qtopss 22988 | A surjective continuous function from π½ to πΎ induces a topology π½ qTop πΉ on the base set of πΎ. This topology is in general finer than πΎ. Together with qtopid 22978, this implies that π½ qTop πΉ is the finest topology making πΉ continuous, i.e. the final topology with respect to the family {πΉ}. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ ((πΉ β (π½ Cn πΎ) β§ πΎ β (TopOnβπ) β§ ran πΉ = π) β πΎ β (π½ qTop πΉ)) | ||
Theorem | qtopeu 22989* | Universal property of the quotient topology. If πΊ is a function from π½ to πΎ which is equal on all equivalent elements under πΉ, then there is a unique continuous map π:(π½ / πΉ)βΆπΎ such that πΊ = π β πΉ, and we say that πΊ "passes to the quotient". (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ:πβontoβπ) & β’ (π β πΊ β (π½ Cn πΎ)) & β’ ((π β§ (π₯ β π β§ π¦ β π β§ (πΉβπ₯) = (πΉβπ¦))) β (πΊβπ₯) = (πΊβπ¦)) β β’ (π β β!π β ((π½ qTop πΉ) Cn πΎ)πΊ = (π β πΉ)) | ||
Theorem | qtoprest 22990 | If π΄ is a saturated open or closed set (where saturated means that π΄ = (β‘πΉ β π) for some π), then the restriction of the quotient map πΉ to π΄ is a quotient map. (Contributed by Mario Carneiro, 24-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ:πβontoβπ) & β’ (π β π β π) & β’ (π β π΄ = (β‘πΉ β π)) & β’ (π β (π΄ β π½ β¨ π΄ β (Clsdβπ½))) β β’ (π β ((π½ qTop πΉ) βΎt π) = ((π½ βΎt π΄) qTop (πΉ βΎ π΄))) | ||
Theorem | qtopomap 22991* | If πΉ is a surjective continuous open map, then it is a quotient map. (An open map is a function that maps open sets to open sets.) (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β ran πΉ = π) & β’ ((π β§ π₯ β π½) β (πΉ β π₯) β πΎ) β β’ (π β πΎ = (π½ qTop πΉ)) | ||
Theorem | qtopcmap 22992* | If πΉ is a surjective continuous closed map, then it is a quotient map. (A closed map is a function that maps closed sets to closed sets.) (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ β (π½ Cn πΎ)) & β’ (π β ran πΉ = π) & β’ ((π β§ π₯ β (Clsdβπ½)) β (πΉ β π₯) β (ClsdβπΎ)) β β’ (π β πΎ = (π½ qTop πΉ)) | ||
Theorem | imastopn 22993 | The topology of an image structure. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β π) & β’ π½ = (TopOpenβπ ) & β’ π = (TopOpenβπ) β β’ (π β π = (π½ qTop πΉ)) | ||
Theorem | imastps 22994 | The image of a topological space under a function is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (π β π = (πΉ βs π )) & β’ (π β π = (Baseβπ )) & β’ (π β πΉ:πβontoβπ΅) & β’ (π β π β TopSp) β β’ (π β π β TopSp) | ||
Theorem | qustps 22995 | A quotient structure is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ (π β π = (π /s πΈ)) & β’ (π β π = (Baseβπ )) & β’ (π β πΈ β π) & β’ (π β π β TopSp) β β’ (π β π β TopSp) | ||
Theorem | kqfval 22996* | Value of the function appearing in df-kq 22967. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β π β§ π΄ β π) β (πΉβπ΄) = {π¦ β π½ β£ π΄ β π¦}) | ||
Theorem | kqfeq 22997* | Two points in the Kolmogorov quotient are equal iff the original points are topologically indistinguishable. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ ((π½ β π β§ π΄ β π β§ π΅ β π) β ((πΉβπ΄) = (πΉβπ΅) β βπ¦ β π½ (π΄ β π¦ β π΅ β π¦))) | ||
Theorem | kqffn 22998* | The topological indistinguishability map is a function on the base. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β π β πΉ Fn π) | ||
Theorem | kqval 22999* | Value of the quotient topology function. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β (KQβπ½) = (π½ qTop πΉ)) | ||
Theorem | kqtopon 23000* | The Kolmogorov quotient is a topology on the quotient set. (Contributed by Mario Carneiro, 25-Aug-2015.) |
β’ πΉ = (π₯ β π β¦ {π¦ β π½ β£ π₯ β π¦}) β β’ (π½ β (TopOnβπ) β (KQβπ½) β (TopOnβran πΉ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |