![]() |
Metamath
Proof Explorer Theorem List (p. 234 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ptuni2 23301* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ β π΄ βͺ (πΉβπ) = βͺ π΅) | ||
Theorem | ptbasin 23302* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (π β π΅ β§ π β π΅)) β (π β© π) β π΅) | ||
Theorem | ptbasin2 23303* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β (fiβπ΅) = π΅) | ||
Theorem | ptbas 23304* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β π΅ β TopBases) | ||
Theorem | ptpjpre2 23305* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} & β’ π = Xπ β π΄ βͺ (πΉβπ) β β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (β‘(π€ β π β¦ (π€βπΌ)) β π) β π΅) | ||
Theorem | ptbasfi 23306* | The basis for the product topology can also be written as the set of finite intersections of "cylinder sets", the preimages of projections into one factor from open sets in the factor. (We have to add π itself to the list because if π΄ is empty we get (fiββ ) = β while π΅ = {β }.) (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} & β’ π = Xπ β π΄ βͺ (πΉβπ) β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β π΅ = (fiβ({π} βͺ ran (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’))))) | ||
Theorem | pttop 23307 | The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β (βtβπΉ) β Top) | ||
Theorem | ptopn 23308* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆTop) & β’ (π β π β Fin) & β’ ((π β§ π β π΄) β π β (πΉβπ)) & β’ ((π β§ π β (π΄ β π)) β π = βͺ (πΉβπ)) β β’ (π β Xπ β π΄ π β (βtβπΉ)) | ||
Theorem | ptopn2 23309* | A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆTop) & β’ (π β π β (πΉβπ)) β β’ (π β Xπ β π΄ if(π = π, π, βͺ (πΉβπ)) β (βtβπΉ)) | ||
Theorem | xkotf 23310* | Functionality of function π. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π & β’ πΎ = {π₯ β π« π β£ (π βΎt π₯) β Comp} & β’ π = (π β πΎ, π£ β π β¦ {π β (π Cn π) β£ (π β π) β π£}) β β’ π:(πΎ Γ π)βΆπ« (π Cn π) | ||
Theorem | xkobval 23311* | Alternative expression for the subbase of the compact-open topology. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ π = βͺ π & β’ πΎ = {π₯ β π« π β£ (π βΎt π₯) β Comp} & β’ π = (π β πΎ, π£ β π β¦ {π β (π Cn π) β£ (π β π) β π£}) β β’ ran π = {π β£ βπ β π« πβπ£ β π ((π βΎt π) β Comp β§ π = {π β (π Cn π) β£ (π β π) β π£})} | ||
Theorem | xkoval 23312* | Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π & β’ πΎ = {π₯ β π« π β£ (π βΎt π₯) β Comp} & β’ π = (π β πΎ, π£ β π β¦ {π β (π Cn π) β£ (π β π) β π£}) β β’ ((π β Top β§ π β Top) β (π βko π ) = (topGenβ(fiβran π))) | ||
Theorem | xkotop 23313 | The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π β Top β§ π β Top) β (π βko π ) β Top) | ||
Theorem | xkoopn 23314* | A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π & β’ (π β π β Top) & β’ (π β π β Top) & β’ (π β π΄ β π) & β’ (π β (π βΎt π΄) β Comp) & β’ (π β π β π) β β’ (π β {π β (π Cn π) β£ (π β π΄) β π} β (π βko π )) | ||
Theorem | txtopi 23315 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ π β Top & β’ π β Top β β’ (π Γt π) β Top | ||
Theorem | txtopon 23316 | The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 22-Aug-2015.) (Revised by Mario Carneiro, 2-Sep-2015.) |
β’ ((π β (TopOnβπ) β§ π β (TopOnβπ)) β (π Γt π) β (TopOnβ(π Γ π))) | ||
Theorem | txuni 23317 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = βͺ π & β’ π = βͺ π β β’ ((π β Top β§ π β Top) β (π Γ π) = βͺ (π Γt π)) | ||
Theorem | txunii 23318 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ π β Top & β’ π β Top & β’ π = βͺ π & β’ π = βͺ π β β’ (π Γ π) = βͺ (π Γt π) | ||
Theorem | ptuni 23319* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π½ = (βtβπΉ) β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ₯ β π΄ βͺ (πΉβπ₯) = βͺ π½) | ||
Theorem | ptunimpt 23320* | Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ π½ = (βtβ(π₯ β π΄ β¦ πΎ)) β β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β Top) β Xπ₯ β π΄ βͺ πΎ = βͺ π½) | ||
Theorem | pttopon 23321* | The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ π½ = (βtβ(π₯ β π΄ β¦ πΎ)) β β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β (TopOnβπ΅)) β π½ β (TopOnβXπ₯ β π΄ π΅)) | ||
Theorem | pttoponconst 23322 | The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ π½ = (βtβ(π΄ Γ {π })) β β’ ((π΄ β π β§ π β (TopOnβπ)) β π½ β (TopOnβ(π βm π΄))) | ||
Theorem | ptuniconst 23323 | The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π½ = (βtβ(π΄ Γ {π })) & β’ π = βͺ π β β’ ((π΄ β π β§ π β Top) β (π βm π΄) = βͺ π½) | ||
Theorem | xkouni 23324 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π½ = (π βko π ) β β’ ((π β Top β§ π β Top) β (π Cn π) = βͺ π½) | ||
Theorem | xkotopon 23325 | The base set of the compact-open topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ π½ = (π βko π ) β β’ ((π β Top β§ π β Top) β π½ β (TopOnβ(π Cn π))) | ||
Theorem | ptval2 23326* | The value of the product topology function. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ π½ = (βtβπΉ) & β’ π = βͺ π½ & β’ πΊ = (π β π΄, π’ β (πΉβπ) β¦ (β‘(π€ β π β¦ (π€βπ)) β π’)) β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β π½ = (topGenβ(fiβ({π} βͺ ran πΊ)))) | ||
Theorem | txopn 23327 | The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ (((π β π β§ π β π) β§ (π΄ β π β§ π΅ β π)) β (π΄ Γ π΅) β (π Γt π)) | ||
Theorem | txcld 23328 | The product of two closed sets is closed in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 3-Sep-2015.) |
β’ ((π΄ β (Clsdβπ ) β§ π΅ β (Clsdβπ)) β (π΄ Γ π΅) β (Clsdβ(π Γt π))) | ||
Theorem | txcls 23329 | Closure of a rectangle in the product topology. (Contributed by Mario Carneiro, 17-Sep-2015.) |
β’ (((π β (TopOnβπ) β§ π β (TopOnβπ)) β§ (π΄ β π β§ π΅ β π)) β ((clsβ(π Γt π))β(π΄ Γ π΅)) = (((clsβπ )βπ΄) Γ ((clsβπ)βπ΅))) | ||
Theorem | txss12 23330 | Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ (((π΅ β π β§ π· β π) β§ (π΄ β π΅ β§ πΆ β π·)) β (π΄ Γt πΆ) β (π΅ Γt π·)) | ||
Theorem | txbasval 23331 | It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014.) |
β’ ((π β π β§ π β π) β ((topGenβπ ) Γt (topGenβπ)) = (π Γt π)) | ||
Theorem | neitx 23332 | The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018.) |
β’ π = βͺ π½ & β’ π = βͺ πΎ β β’ (((π½ β Top β§ πΎ β Top) β§ (π΄ β ((neiβπ½)βπΆ) β§ π΅ β ((neiβπΎ)βπ·))) β (π΄ Γ π΅) β ((neiβ(π½ Γt πΎ))β(πΆ Γ π·))) | ||
Theorem | txcnpi 23333* | Continuity of a two-argument function at a point. (Contributed by Mario Carneiro, 20-Sep-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β πΉ β (((π½ Γt πΎ) CnP πΏ)ββ¨π΄, π΅β©)) & β’ (π β π β πΏ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β (π΄πΉπ΅) β π) β β’ (π β βπ’ β π½ βπ£ β πΎ (π΄ β π’ β§ π΅ β π£ β§ (π’ Γ π£) β (β‘πΉ β π))) | ||
Theorem | tx1cn 23334 | Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.) |
β’ ((π β (TopOnβπ) β§ π β (TopOnβπ)) β (1st βΎ (π Γ π)) β ((π Γt π) Cn π )) | ||
Theorem | tx2cn 23335 | 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 23336* | 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 23337* | The projection map is an open map. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π = βͺ π½ & β’ π½ = (βtβπΉ) β β’ (((π΄ β π β§ πΉ:π΄βΆTop β§ πΌ β π΄) β§ π β π½) β ((π₯ β π β¦ (π₯βπΌ)) β π) β (πΉβπΌ)) | ||
Theorem | ptcld 23338* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆTop) & β’ ((π β§ π β π΄) β πΆ β (Clsdβ(πΉβπ))) β β’ (π β Xπ β π΄ πΆ β (Clsdβ(βtβπΉ))) | ||
Theorem | ptcldmpt 23339* | A closed box in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π΄ β π) & β’ ((π β§ π β π΄) β π½ β Top) & β’ ((π β§ π β π΄) β πΆ β (Clsdβπ½)) β β’ (π β Xπ β π΄ πΆ β (Clsdβ(βtβ(π β π΄ β¦ π½)))) | ||
Theorem | ptclsg 23340* | 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 23341* | 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 23342* | Lemma for dfac14 23343. 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 23341 to extract an element of the closure of Xπ β πΌπ. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ (π β πΌ β π) & β’ ((π β§ π₯ β πΌ) β π β π) & β’ ((π β§ π₯ β πΌ) β π β β ) & β’ π = π« βͺ π & β’ π = {π¦ β π« (π βͺ {π}) β£ (π β π¦ β π¦ = (π βͺ {π}))} & β’ π½ = (βtβ(π₯ β πΌ β¦ π )) & β’ (π β ((clsβπ½)βXπ₯ β πΌ π) = Xπ₯ β πΌ ((clsβπ )βπ)) β β’ (π β Xπ₯ β πΌ π β β ) | ||
Theorem | dfac14 23343* | Theorem ptcls 23341 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 23344* | 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 23345* | 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 23346* | Lemma for ptcnp 23347. (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ πΎ = (βtβπΉ) & β’ (π β π½ β (TopOnβπ)) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβΆTop) & β’ (π β π· β π) & β’ ((π β§ π β πΌ) β (π₯ β π β¦ π΄) β ((π½ CnP (πΉβπ))βπ·)) & β’ β²ππ & β’ ((π β§ π) β πΊ Fn πΌ) & β’ (((π β§ π) β§ π β πΌ) β (πΊβπ) β (πΉβπ)) & β’ ((π β§ π) β π β Fin) & β’ (((π β§ π) β§ π β (πΌ β π)) β (πΊβπ) = βͺ (πΉβπ)) & β’ ((π β§ π) β ((π₯ β π β¦ (π β πΌ β¦ π΄))βπ·) β Xπ β πΌ (πΊβπ)) β β’ ((π β§ π) β βπ§ β π½ (π· β π§ β§ ((π₯ β π β¦ (π β πΌ β¦ π΄)) β π§) β Xπ β πΌ (πΊβπ))) | ||
Theorem | ptcnp 23347* | 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 23348* | 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 23349* | 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 23350* | 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 23351 | 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 23352* | 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 23353 | Topology of a structure product. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π Fn πΌ) & β’ π = (TopOpenβπ) β β’ (π β π = (βtβ(TopOpen β π ))) | ||
Theorem | prdstps 23354 | A structure product of topological spaces is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (πXsπ ) & β’ (π β π β π) & β’ (π β πΌ β π) & β’ (π β π :πΌβΆTopSp) β β’ (π β π β TopSp) | ||
Theorem | pwstps 23355 | A structure power of a topological space is a topological space. (Contributed by Mario Carneiro, 27-Aug-2015.) |
β’ π = (π βs πΌ) β β’ ((π β TopSp β§ πΌ β π) β π β TopSp) | ||
Theorem | txrest 23356 | 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 23357 | The topological product of discrete spaces is discrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ((π΄ β π β§ π΅ β π) β (π« π΄ Γt π« π΅) = π« (π΄ Γ π΅)) | ||
Theorem | txindislem 23358 | Lemma for txindis 23359. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ (( I βπ΄) Γ ( I βπ΅)) = ( I β(π΄ Γ π΅)) | ||
Theorem | txindis 23359 | The topological product of indiscrete spaces is indiscrete. (Contributed by Mario Carneiro, 14-Aug-2015.) |
β’ ({β , π΄} Γt {β , π΅}) = {β , (π΄ Γ π΅)} | ||
Theorem | txdis1cn 23360* | 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 23361* | 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 23362* | 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 23363 | The product of a collection of Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆHaus) β (βtβπΉ) β Haus) | ||
Theorem | ptrescn 23364* | Restriction is a continuous function on product topologies. (Contributed by Mario Carneiro, 7-Feb-2015.) |
β’ π = βͺ π½ & β’ π½ = (βtβπΉ) & β’ πΎ = (βtβ(πΉ βΎ π΅)) β β’ ((π΄ β π β§ πΉ:π΄βΆTop β§ π΅ β π΄) β (π₯ β π β¦ (π₯ βΎ π΅)) β (π½ Cn πΎ)) | ||
Theorem | txtube 23365* | 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 23366* | Lemma for txcmp 23368. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π & β’ π = βͺ π & β’ (π β π β Comp) & β’ (π β π β Comp) & β’ (π β π β (π Γt π)) & β’ (π β (π Γ π) = βͺ π) & β’ (π β π΄ β π) β β’ (π β βπ’ β π (π΄ β π’ β§ βπ£ β (π« π β© Fin)(π Γ π’) β βͺ π£)) | ||
Theorem | txcmplem2 23367* | Lemma for txcmp 23368. (Contributed by Mario Carneiro, 14-Sep-2014.) |
β’ π = βͺ π & β’ π = βͺ π & β’ (π β π β Comp) & β’ (π β π β Comp) & β’ (π β π β (π Γt π)) & β’ (π β (π Γ π) = βͺ π) β β’ (π β βπ£ β (π« π β© Fin)(π Γ π) = βͺ π£) | ||
Theorem | txcmp 23368 | 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 23369 | 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 23370 | 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 23371 | 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 23372 | The topological product of two Hausdorff spaces is Hausdorff. (Contributed by Mario Carneiro, 23-Mar-2015.) |
β’ ((π β Haus β§ π β Haus) β (π Γt π) β Haus) | ||
Theorem | txlm 23373* | 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 23374* | 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 23375 | The topological product of two first-countable spaces is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π β 1stΟ β§ π β 1stΟ) β (π Γt π) β 1stΟ) | ||
Theorem | tx2ndc 23376 | The topological product of two second-countable spaces is second-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π β 2ndΟ β§ π β 2ndΟ) β (π Γt π) β 2ndΟ) | ||
Theorem | txkgen 23377 | 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 23378 | 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 23379 | 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 23380 | 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 23381* | 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 23409.) (Contributed by Mario Carneiro, 3-Feb-2015.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ π = βͺ π β β’ ((π β Top β§ π β Top β§ π΄ β π) β (π β (π Cn π) β¦ (πβπ΄)) β ((π βko π ) Cn π)) | ||
Theorem | xkoco1cn 23382* | If πΉ is a continuous function, then π β¦ π β πΉ is a continuous function on function spaces. (The reason we prove this and xkoco2cn 23383 independently of the more general xkococn 23385 is because that requires some inconvenient extra assumptions on π.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β Top) & β’ (π β πΉ β (π Cn π)) β β’ (π β (π β (π Cn π) β¦ (π β πΉ)) β ((π βko π) Cn (π βko π ))) | ||
Theorem | xkoco2cn 23383* | 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 23384* | 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 23385* | 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 23386* | The identity function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) β β’ (π β (π₯ β π β¦ π₯) β (π½ Cn π½)) | ||
Theorem | cnmptc 23387* | A constant function is continuous. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 22-Aug-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΎ β (TopOnβπ)) & β’ (π β π β π) β β’ (π β (π₯ β π β¦ π) β (π½ Cn πΎ)) | ||
Theorem | cnmpt11 23388* | 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 23389* | 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 23390* | 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 23391* | 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 23392* | 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 23393* | 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 23394* | 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 23395* | 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 23396* | 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 23397* | 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 23398* | 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 23399* | 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 23400* | 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 π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |