![]() |
Metamath
Proof Explorer Theorem List (p. 236 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | tx2cn 23501 | Continuity of the second projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
β’ ((π β (TopOnβπ) β§ π β (TopOnβπ)) β (2nd βΎ (π Γ π)) β ((π Γt π) Cn π)) | ||
Theorem | ptpjcn 23502* | Continuity of a projection map into a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Feb-2015.) |
β’ π = βͺ π½ & β’ π½ = (βtβπΉ) β β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ πΌ β π΄) β (π₯ β π β¦ (π₯βπΌ)) β (π½ Cn (πΉβπΌ))) | ||
Theorem | ptpjopn 23503* | The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = βͺ π½ & β’ π½ = (βtβπΉ) β β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ πΌ β π΄) β§ π β π½) β ((π₯ β π β¦ (π₯βπΌ)) β π) β (πΉβπΌ)) | ||
Theorem | ptcld 23504* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆTop) & β’ ((π β§ π β π΄) β πΆ β (Clsdβ(πΉβπ))) β β’ (π β Xπ β π΄ πΆ β (Clsdβ(βtβπΉ))) | ||
Theorem | ptcldmpt 23505* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π½ β Top) & β’ ((π β§ π β π΄) β πΆ β (Clsdβπ½)) β β’ (π β Xπ β π΄ πΆ β (Clsdβ(βtβ(π β π΄ β¦ π½)))) | ||
Theorem | ptclsg 23506* | The closure of a box in the product topology is the box formed from the closures of the factors. The proof uses the axiom of choice; the last hypothesis is the choice assumption. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ π½ = (βtβ(π β π΄ β¦ π )) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π β (TopOnβπ)) & β’ ((π β§ π β π΄) β π β π) & β’ (π β βͺ π β π΄ π β AC π΄) β β’ (π β ((clsβπ½)βXπ β π΄ π) = Xπ β π΄ ((clsβπ )βπ)) | ||
Theorem | ptcls 23507* | The closure of a box in the product topology is the box formed from the closures of the factors. This theorem is an AC equivalent. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π½ = (βtβ(π β π΄ β¦ π )) & β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π β (TopOnβπ)) & β’ ((π β§ π β π΄) β π β π) β β’ (π β ((clsβπ½)βXπ β π΄ π) = Xπ β π΄ ((clsβπ )βπ)) | ||
Theorem | dfac14lem 23508* | Lemma for dfac14 23509. By equipping π βͺ {π} for some π β π with the particular point topology, we can show that π is in the closure of π; hence the sequence π(π₯) is in the product of the closures, and we can utilize this instance of ptcls 23507 to extract an element of the closure of Xπ β πΌπ. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ (π β πΌ β π) & β’ ((π β§ π₯ β πΌ) β π β π) & β’ ((π β§ π₯ β πΌ) β π β β ) & β’ π = π« βͺ π & β’ π = {π¦ β π« (π βͺ {π}) β£ (π β π¦ β π¦ = (π βͺ {π}))} & β’ π½ = (βtβ(π₯ β πΌ β¦ π )) & β’ (π β ((clsβπ½)βXπ₯ β πΌ π) = Xπ₯ β πΌ ((clsβπ )βπ)) β β’ (π β Xπ₯ β πΌ π β β ) | ||
Theorem | dfac14 23509* | Theorem ptcls 23507 is an equivalent of the axiom of choice. (Contributed by Mario Carneiro, 3-Sep-2015.) |
β’ (CHOICE β βπ(π:dom πβΆTop β βπ β X π β dom ππ« βͺ (πβπ)((clsβ(βtβπ))βXπ β dom π(π βπ)) = Xπ β dom π((clsβ(πβπ))β(π βπ)))) | ||
Theorem | xkoccn 23510* | The "constant function" function which maps π₯ β π to the constant function π§ β π β¦ π₯ is a continuous function from π into the space of continuous functions from π to π. This can also be understood as the currying of the first projection function. (The currying of the second projection function is π₯ β π β¦ (π§ β π β¦ π§), which we already know is continuous because it is a constant function.) (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π β (TopOnβπ) β§ π β (TopOnβπ)) β (π₯ β π β¦ (π Γ {π₯})) β (π Cn (π βko π ))) | ||
Theorem | txcnp 23511* | If two functions are continuous at π·, then the ordered pair of them is continuous at π· into the product topology. (Contributed by Mario Carneiro, 9-Aug-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΏ β (TopOnβπ)) & β’ (π β π· β π) & β’ (π β (π₯ β π β¦ π΄) β ((π½ CnP πΎ)βπ·)) & β’ (π β (π₯ β π β¦ π΅) β ((π½ CnP πΏ)βπ·)) β β’ (π β (π₯ β π β¦ β¨π΄, π΅β©) β ((π½ CnP (πΎ Γt πΏ))βπ·)) | ||
Theorem | ptcnplem 23512* | Lemma for ptcnp 23513. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ πΎ = (βtβπΉ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβΆTop) & β’ (π β π· β π) & β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) & β’ β²ππ & β’ ((π β§ π) β πΊ Fn πΌ) & β’ (((π β§ π) β§ π β πΌ) β (πΊβπ) β (πΉβπ)) & β’ ((π β§ π) β π β Fin) & β’ (((π β§ π) β§ π β (πΌ β π)) β (πΊβπ) = βͺ (πΉβπ)) & β’ ((π β§ π) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πΊβπ)) β β’ ((π β§ π) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πΊβπ))) | ||
Theorem | ptcnp 23513* | If every projection of a function is continuous at π·, then the function itself is continuous at π· into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ πΎ = (βtβπΉ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβΆTop) & β’ (π β π· β π) & β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) β β’ (π β (π₯ β π β¦ (π β πΌ β¦ π΄)) β ((π½ CnP πΎ)βπ·)) | ||
Theorem | upxp 23514* | Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.) |
β’ π = (1st βΎ (π΅ Γ πΆ)) & β’ π = (2nd βΎ (π΅ Γ πΆ)) β β’ ((π΄ β π· β§ πΉ:π΄βΆπ΅ β§ πΊ:π΄βΆπΆ) β β!β(β:π΄βΆ(π΅ Γ πΆ) β§ πΉ = (π β β) β§ πΊ = (π β β))) | ||
Theorem | txcnmpt 23515* | A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π & β’ π» = (π₯ β π β¦ β¨(πΉβπ₯), (πΊβπ₯)β©) β β’ ((πΉ β (π Cn π ) β§ πΊ β (π Cn π)) β π» β (π Cn (π Γt π))) | ||
Theorem | uptx 23516* | Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
β’ π = (π Γt π) & β’ π = βͺ π & β’ π = βͺ π & β’ π = (π Γ π) & β’ π = (1st βΎ π) & β’ π = (2nd βΎ π) β β’ ((πΉ β (π Cn π ) β§ πΊ β (π Cn π)) β β!β β (π Cn π)(πΉ = (π β β) β§ πΊ = (π β β))) | ||
Theorem | txcn 23517 | A map into the product of two topological spaces is continuous iff both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π & β’ π = βͺ π & β’ π = (π Γ π) & β’ π = βͺ π & β’ π = (1st βΎ π) & β’ π = (2nd βΎ π) β β’ ((π β Top β§ π β Top β§ πΉ:πβΆπ) β (πΉ β (π Cn (π Γt π)) β ((π β πΉ) β (π Cn π ) β§ (π β πΉ) β (π Cn π)))) | ||
Theorem | ptcn 23518* | If every projection of a function is continuous, then the function itself is continuous into the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ πΎ = (βtβπΉ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβΆTop) & β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄) β (π½ Cn (πΉβπ))) β β’ (π β (π₯ β π β¦ (π β πΌ β¦ π΄)) β (π½ Cn πΎ)) | ||
Theorem | prdstopn 23519 | Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ π = (TopOpenβπ) β β’ (π β π = (βtβ(TopOpen β π ))) | ||
Theorem | prdstps 23520 | A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆTopSp) β β’ (π β π β TopSp) | ||
Theorem | pwstps 23521 | A structure power of a topological space is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β TopSp β§ πΌ β π) β π β TopSp) | ||
Theorem | txrest 23522 | 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 23523 | The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (π« π΄ Γt π« π΅) = π« (π΄ Γ π΅)) | ||
Theorem | txindislem 23524 | Lemma for txindis 23525. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (( I βπ΄) Γ ( I βπ΅)) = ( I β(π΄ Γ π΅)) | ||
Theorem | txindis 23525 | The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ({β , π΄} Γt {β , π΅}) = {β , (π΄ Γ π΅)} | ||
Theorem | txdis1cn 23526* | 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 23527* | 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 23528* | 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 23529 | The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆHaus) β (βtβπΉ) β Haus) | ||
Theorem | ptrescn 23530* | Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ π = βͺ π½ & β’ π½ = (βtβπΉ) & β’ πΎ = (βtβ(πΉ βΎ π΅)) β β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (π₯ β π β¦ (π₯ βΎ π΅)) β (π½ Cn πΎ)) | ||
Theorem | txtube 23531* | 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 23532* | Lemma for txcmp 23534. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π & β’ π = βͺ π & β’ (π β π β Comp) & β’ (π β π β Comp) & β’ (π β π β (π Γt π)) & β’ (π β (π Γ π) = βͺ π) & β’ (π β π΄ β π) β β’ (π β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) | ||
Theorem | txcmplem2 23533* | Lemma for txcmp 23534. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π & β’ π = βͺ π & β’ (π β π β Comp) & β’ (π β π β Comp) & β’ (π β π β (π Γt π)) & β’ (π β (π Γ π) = βͺ π) β β’ (π β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£) | ||
Theorem | txcmp 23534 | 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 23535 | 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 23536 | 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 23537 | 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 23538 | The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π β Haus β§ π β Haus) β (π Γt π) β Haus) | ||
Theorem | txlm 23539* | 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 23540* | 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 23541 | The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π β 1stΟ β§ π β 1stΟ) β (π Γt π) β 1stΟ) | ||
Theorem | tx2ndc 23542 | The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π β 2ndΟ β§ π β 2ndΟ) β (π Γt π) β 2ndΟ) | ||
Theorem | txkgen 23543 | 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 23544 | 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 23545 | 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 23546 | 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 23547* | 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 23575.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π β β’ ((π β Top β§ π β Top β§ π΄ β π) β (π β (π Cn π) β¦ (πβπ΄)) β ((π βko π ) Cn π)) | ||
Theorem | xkoco1cn 23548* | If πΉ is a continuous function, then π β¦ π β πΉ is a continuous function on function spaces. (The reason we prove this and xkoco2cn 23549 independently of the more general xkococn 23551 is because that requires some inconvenient extra assumptions on π.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β Top) & β’ (π β πΉ β (π Cn π)) β β’ (π β (π β (π Cn π) β¦ (π β πΉ)) β ((π βko π) Cn (π βko π ))) | ||
Theorem | xkoco2cn 23549* | 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 23550* | 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 23551* | 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 23552* | The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) β β’ (π β (π₯ β π β¦ π₯) β (π½ Cn π½)) | ||
Theorem | cnmptc 23553* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (π₯ β π β¦ π) β (π½ Cn πΎ)) | ||
Theorem | cnmpt11 23554* | 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 23555* | 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 23556* | 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 23557* | 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 23558* | 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 23559* | 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 23560* | 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 23561* | 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 23562* | 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 23563* | 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 23564* | 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 23565* | 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 23566* | 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 23567* | The restriction of a continuous function to a subset is continuous. (Contributed by Mario Carneiro, 5-Jun-2014.) |
β’ πΎ = (π½ βΎt π) & β’ (π β π½ β (TopOnβπ)) & β’ (π β π β π) & β’ (π β (π₯ β π β¦ π΄) β (π½ Cn πΏ)) β β’ (π β (π₯ β π β¦ π΄) β (πΎ Cn πΏ)) | ||
Theorem | cnmpt2res 23568* | 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 23569* | The argument converse of a continuous function is continuous. (Contributed by Mario Carneiro, 6-Jun-2014.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β β’ (π β (π¦ β π, π₯ β π β¦ π΄) β ((πΎ Γt π½) Cn πΏ)) | ||
Theorem | cnmptkc 23570* | 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 23571* | 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 23572* | 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 23573* | 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 23574* | 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 23575* | Joint continuity of the function value operation as a function on continuous function spaces. (Compare xkopjcn 23547.) (Contributed by Mario Carneiro, 20-Mar-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π & β’ πΉ = (π β (π Cn π), π₯ β π β¦ (πβπ₯)) β β’ ((π β π-Locally Comp β§ π β Top) β πΉ β (((π βko π ) Γt π ) Cn π)) | ||
Theorem | cnmptk1p 23576* | 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 23577* | 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 23578* | 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 23579* | The currying of a two-argument function is continuous. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β (π₯ β π, π¦ β π β¦ π΄) β ((π½ Γt πΎ) Cn πΏ)) β β’ (π β (π₯ β π β¦ (π¦ β π β¦ π΄)) β (π½ Cn (πΏ βko πΎ))) | ||
Theorem | txconn 23580 | The topological product of two connected spaces is connected. (Contributed by Mario Carneiro, 29-Mar-2015.) |
β’ ((π β Conn β§ π β Conn) β (π Γt π) β Conn) | ||
Theorem | imasnopn 23581 | 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 23582 | 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 23583 | 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 23584 | Extend class notation with the Kolmogorov quotient function. |
class KQ | ||
Definition | df-kq 23585* | 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 23586* | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ β π) β (π½ qTop πΉ) = {π β π« (πΉ β π) β£ ((β‘πΉ β π ) β© π) β π½}) | ||
Theorem | qtopval2 23587* | 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 23588 | Value of the quotient topology function. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ β§ π β π) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtopres 23589 | 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 23590 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π½ β Top β§ πΉ β π β§ Fun πΉ) β (π½ qTop πΉ) β Top) | ||
Theorem | qtoptop 23591 | The quotient topology is a topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ Fn π) β (π½ qTop πΉ) β Top) | ||
Theorem | elqtop2 23592 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β π β§ πΉ:πβontoβπ) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtopuni 23593 | The base set of the quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Top β§ πΉ:πβontoβπ) β π = βͺ (π½ qTop πΉ)) | ||
Theorem | elqtop3 23594 | Value of the quotient topology function. (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π΄ β (π½ qTop πΉ) β (π΄ β π β§ (β‘πΉ β π΄) β π½))) | ||
Theorem | qtoptopon 23595 | The base set of the quotient topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ:πβontoβπ) β (π½ qTop πΉ) β (TopOnβπ)) | ||
Theorem | qtopid 23596 | A quotient map is a continuous function into its quotient topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΉ Fn π) β πΉ β (π½ Cn (π½ qTop πΉ))) | ||
Theorem | idqtop 23597 | The quotient topology induced by the identity function is the original topology. (Contributed by Mario Carneiro, 30-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (π½ qTop ( I βΎ π)) = π½) | ||
Theorem | qtopcmplem 23598 | Lemma for qtopcmp 23599 and qtopconn 23600. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ & β’ (π½ β π΄ β π½ β Top) & β’ ((π½ β π΄ β§ πΉ:πβontoββͺ (π½ qTop πΉ) β§ πΉ β (π½ Cn (π½ qTop πΉ))) β (π½ qTop πΉ) β π΄) β β’ ((π½ β π΄ β§ πΉ Fn π) β (π½ qTop πΉ) β π΄) | ||
Theorem | qtopcmp 23599 | A quotient of a compact space is compact. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Comp β§ πΉ Fn π) β (π½ qTop πΉ) β Comp) | ||
Theorem | qtopconn 23600 | A quotient of a connected space is connected. (Contributed by Mario Carneiro, 24-Mar-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Conn β§ πΉ Fn π) β (π½ qTop πΉ) β Conn) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |