![]() |
Metamath
Proof Explorer Theorem List (p. 231 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | disllycmp 23001 | A discrete space is locally compact. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π β π β π« π β Locally Comp) | ||
Theorem | dis1stc 23002 | A discrete space is first-countable. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π β π β π« π β 1stΟ) | ||
Theorem | hausmapdom 23003 | If π is a first-countable Hausdorff space, then the cardinality of the closure of a set π΄ is bounded by β to the power π΄. In particular, a first-countable Hausdorff space with a dense subset π΄ has cardinality at most π΄ββ, and a separable first-countable Hausdorff space has cardinality at most π« β. (Compare hauspwpwdom 23491 to see a weaker result if the assumption of first-countability is omitted.) (Contributed by Mario Carneiro, 9-Apr-2015.) |
β’ π = βͺ π½ β β’ ((π½ β Haus β§ π½ β 1stΟ β§ π΄ β π) β ((clsβπ½)βπ΄) βΌ (π΄ βm β)) | ||
Theorem | hauspwdom 23004 | Simplify the cardinal π΄ββ of hausmapdom 23003 to π« π΅ = 2βπ΅ when π΅ is an infinite cardinal greater than π΄. (Contributed by Mario Carneiro, 9-Apr-2015.) (Revised by Mario Carneiro, 30-Apr-2015.) |
β’ π = βͺ π½ β β’ (((π½ β Haus β§ π½ β 1stΟ β§ π΄ β π) β§ (π΄ βΌ π« π΅ β§ β βΌ π΅)) β ((clsβπ½)βπ΄) βΌ π« π΅) | ||
Syntax | cref 23005 | Extend class definition to include the refinement relation. |
class Ref | ||
Syntax | cptfin 23006 | Extend class definition to include the class of point-finite covers. |
class PtFin | ||
Syntax | clocfin 23007 | Extend class definition to include the class of locally finite covers. |
class LocFin | ||
Definition | df-ref 23008* | Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.) |
β’ Ref = {β¨π₯, π¦β© β£ (βͺ π¦ = βͺ π₯ β§ βπ§ β π₯ βπ€ β π¦ π§ β π€)} | ||
Definition | df-ptfin 23009* | Define "point-finite." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ PtFin = {π₯ β£ βπ¦ β βͺ π₯{π§ β π₯ β£ π¦ β π§} β Fin} | ||
Definition | df-locfin 23010* | Define "locally finite." (Contributed by Jeff Hankins, 21-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ LocFin = (π₯ β Top β¦ {π¦ β£ (βͺ π₯ = βͺ π¦ β§ βπ β βͺ π₯βπ β π₯ (π β π β§ {π β π¦ β£ (π β© π) β β } β Fin))}) | ||
Theorem | refrel 23011 | Refinement is a relation. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ Rel Ref | ||
Theorem | isref 23012* | The property of being a refinement of a cover. Dr. Nyikos once commented in class that the term "refinement" is actually misleading and that people are inclined to confuse it with the notion defined in isfne 35219. On the other hand, the two concepts do seem to have a dual relationship. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄ β πΆ β (π΄Refπ΅ β (π = π β§ βπ₯ β π΄ βπ¦ β π΅ π₯ β π¦))) | ||
Theorem | refbas 23013 | A refinement covers the same set. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ (π΄Refπ΅ β π = π) | ||
Theorem | refssex 23014* | Every set in a refinement has a superset in the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ ((π΄Refπ΅ β§ π β π΄) β βπ₯ β π΅ π β π₯) | ||
Theorem | ssref 23015 | A subcover is a refinement of the original cover. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ π = βͺ π΄ & β’ π = βͺ π΅ β β’ ((π΄ β πΆ β§ π΄ β π΅ β§ π = π) β π΄Refπ΅) | ||
Theorem | refref 23016 | Reflexivity of refinement. (Contributed by Jeff Hankins, 18-Jan-2010.) |
β’ (π΄ β π β π΄Refπ΄) | ||
Theorem | reftr 23017 | Refinement is transitive. (Contributed by Jeff Hankins, 18-Jan-2010.) (Revised by Thierry Arnoux, 3-Feb-2020.) |
β’ ((π΄Refπ΅ β§ π΅RefπΆ) β π΄RefπΆ) | ||
Theorem | refun0 23018 | Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ ((π΄Refπ΅ β§ π΅ β β ) β (π΄ βͺ {β })Refπ΅) | ||
Theorem | isptfin 23019* | The statement "is a point-finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π΄ β β’ (π΄ β π΅ β (π΄ β PtFin β βπ₯ β π {π¦ β π΄ β£ π₯ β π¦} β Fin)) | ||
Theorem | islocfin 23020* | The statement "is a locally finite cover." (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ (π΄ β (LocFinβπ½) β (π½ β Top β§ π = π β§ βπ₯ β π βπ β π½ (π₯ β π β§ {π β π΄ β£ (π β© π) β β } β Fin))) | ||
Theorem | finptfin 23021 | A finite cover is a point-finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ (π΄ β Fin β π΄ β PtFin) | ||
Theorem | ptfinfin 23022* | A point covered by a point-finite cover is only covered by finitely many elements. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π΄ β β’ ((π΄ β PtFin β§ π β π) β {π₯ β π΄ β£ π β π₯} β Fin) | ||
Theorem | finlocfin 23023 | A finite cover of a topological space is a locally finite cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ ((π½ β Top β§ π΄ β Fin β§ π = π) β π΄ β (LocFinβπ½)) | ||
Theorem | locfintop 23024 | A locally finite cover covers a topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ (π΄ β (LocFinβπ½) β π½ β Top) | ||
Theorem | locfinbas 23025 | A locally finite cover must cover the base set of its corresponding topological space. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ & β’ π = βͺ π΄ β β’ (π΄ β (LocFinβπ½) β π = π) | ||
Theorem | locfinnei 23026* | A point covered by a locally finite cover has a neighborhood which intersects only finitely many elements of the cover. (Contributed by Jeff Hankins, 21-Jan-2010.) |
β’ π = βͺ π½ β β’ ((π΄ β (LocFinβπ½) β§ π β π) β βπ β π½ (π β π β§ {π β π΄ β£ (π β© π) β β } β Fin)) | ||
Theorem | lfinpfin 23027 | A locally finite cover is point-finite. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ (π΄ β (LocFinβπ½) β π΄ β PtFin) | ||
Theorem | lfinun 23028 | Adding a finite set preserves locally finite covers. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
β’ ((π΄ β (LocFinβπ½) β§ π΅ β Fin β§ βͺ π΅ β βͺ π½) β (π΄ βͺ π΅) β (LocFinβπ½)) | ||
Theorem | locfincmp 23029 | For a compact space, the locally finite covers are precisely the finite covers. Sadly, this property does not properly characterize all compact spaces. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π½ & β’ π = βͺ πΆ β β’ (π½ β Comp β (πΆ β (LocFinβπ½) β (πΆ β Fin β§ π = π))) | ||
Theorem | unisngl 23030* | Taking the union of the set of singletons recovers the initial set. (Contributed by Thierry Arnoux, 9-Jan-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π π’ = {π₯}} β β’ π = βͺ πΆ | ||
Theorem | dissnref 23031* | The set of singletons is a refinement of any open covering of the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π π’ = {π₯}} β β’ ((π β π β§ βͺ π = π) β πΆRefπ) | ||
Theorem | dissnlocfin 23032* | The set of singletons is locally finite in the discrete topology. (Contributed by Thierry Arnoux, 9-Jan-2020.) |
β’ πΆ = {π’ β£ βπ₯ β π π’ = {π₯}} β β’ (π β π β πΆ β (LocFinβπ« π)) | ||
Theorem | locfindis 23033 | The locally finite covers of a discrete space are precisely the point-finite covers. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ πΆ β β’ (πΆ β (LocFinβπ« π) β (πΆ β PtFin β§ π = π)) | ||
Theorem | locfincf 23034 | A locally finite cover in a coarser topology is locally finite in a finer topology. (Contributed by Jeff Hankins, 22-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π½ β β’ ((πΎ β (TopOnβπ) β§ π½ β πΎ) β (LocFinβπ½) β (LocFinβπΎ)) | ||
Theorem | comppfsc 23035* | A space where every open cover has a point-finite subcover is compact. This is significant in part because it shows half of the proposition that if only half the generalization in the definition of metacompactness (and consequently paracompactness) is performed, one does not obtain any more spaces. (Contributed by Jeff Hankins, 21-Jan-2010.) (Proof shortened by Mario Carneiro, 11-Sep-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β (π½ β Comp β βπ β π« π½(π = βͺ π β βπ β PtFin (π β π β§ π = βͺ π)))) | ||
Syntax | ckgen 23036 | Extend class notation with the compact generator operation. |
class πGen | ||
Definition | df-kgen 23037* | Define the "compact generator", the functor from topological spaces to compactly generated spaces. Also known as the k-ification operation. A set is k-open, i.e. π₯ β (πGenβπ), iff the preimage of π₯ is open in all compact Hausdorff spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ πGen = (π β Top β¦ {π₯ β π« βͺ π β£ βπ β π« βͺ π((π βΎt π) β Comp β (π₯ β© π) β (π βΎt π))}) | ||
Theorem | kgenval 23038* | Value of the compact generator. (The "k" in πGen comes from the name "k-space" for these spaces, after the German word kompakt.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β (TopOnβπ) β (πGenβπ½) = {π₯ β π« π β£ βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π))}) | ||
Theorem | elkgen 23039* | Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β (TopOnβπ) β (π΄ β (πGenβπ½) β (π΄ β π β§ βπ β π« π((π½ βΎt π) β Comp β (π΄ β© π) β (π½ βΎt π))))) | ||
Theorem | kgeni 23040 | Property of the open sets in the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ ((π΄ β (πGenβπ½) β§ (π½ βΎt πΎ) β Comp) β (π΄ β© πΎ) β (π½ βΎt πΎ)) | ||
Theorem | kgentopon 23041 | The compact generator generates a topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ (π½ β (TopOnβπ) β (πGenβπ½) β (TopOnβπ)) | ||
Theorem | kgenuni 23042 | The base set of the compact generator is the same as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π = βͺ π½ β β’ (π½ β Top β π = βͺ (πGenβπ½)) | ||
Theorem | kgenftop 23043 | The compact generator generates a topology. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β Top β (πGenβπ½) β Top) | ||
Theorem | kgenf 23044 | The compact generator is a function on topologies. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ πGen:TopβΆTop | ||
Theorem | kgentop 23045 | A compactly generated space is a topology. (Note: henceforth we will use the idiom "π½ β ran πGen " to denote "π½ is compactly generated", since as we will show a space is compactly generated iff it is in the range of the compact generator.) (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β ran πGen β π½ β Top) | ||
Theorem | kgenss 23046 | The compact generator generates a finer topology than the original. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β Top β π½ β (πGenβπ½)) | ||
Theorem | kgenhaus 23047 | The compact generator generates another Hausdorff topology given a Hausdorff topology to start from. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π½ β Haus β (πGenβπ½) β Haus) | ||
Theorem | kgencmp 23048 | The compact generator topology is the same as the original topology on compact subspaces. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ ((π½ β Top β§ (π½ βΎt πΎ) β Comp) β (π½ βΎt πΎ) = ((πGenβπ½) βΎt πΎ)) | ||
Theorem | kgencmp2 23049 | The compact generator topology has the same compact sets as the original topology. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β Top β ((π½ βΎt πΎ) β Comp β ((πGenβπ½) βΎt πΎ) β Comp)) | ||
Theorem | kgenidm 23050 | The compact generator is idempotent on compactly generated spaces. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β ran πGen β (πGenβπ½) = π½) | ||
Theorem | iskgen2 23051 | A space is compactly generated iff it contains its image under the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ (π½ β ran πGen β (π½ β Top β§ (πGenβπ½) β π½)) | ||
Theorem | iskgen3 23052* | Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of π that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015.) |
β’ π = βͺ π½ β β’ (π½ β ran πGen β (π½ β Top β§ βπ₯ β π« π(βπ β π« π((π½ βΎt π) β Comp β (π₯ β© π) β (π½ βΎt π)) β π₯ β π½))) | ||
Theorem | llycmpkgen2 23053* | A locally compact space is compactly generated. (This variant of llycmpkgen 23055 uses the weaker definition of locally compact, "every point has a compact neighborhood", instead of "every point has a local base of compact neighborhoods".) (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ π = βͺ π½ & β’ (π β π½ β Top) & β’ ((π β§ π₯ β π) β βπ β ((neiβπ½)β{π₯})(π½ βΎt π) β Comp) β β’ (π β π½ β ran πGen) | ||
Theorem | cmpkgen 23054 | A compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π½ β Comp β π½ β ran πGen) | ||
Theorem | llycmpkgen 23055 | A locally compact space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π½ β π-Locally Comp β π½ β ran πGen) | ||
Theorem | 1stckgenlem 23056 | The one-point compactification of β is compact. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π β π½ β (TopOnβπ)) & β’ (π β πΉ:ββΆπ) & β’ (π β πΉ(βπ‘βπ½)π΄) β β’ (π β (π½ βΎt (ran πΉ βͺ {π΄})) β Comp) | ||
Theorem | 1stckgen 23057 | A first-countable space is compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (π½ β 1stΟ β π½ β ran πGen) | ||
Theorem | kgen2ss 23058 | The compact generator preserves the subset (fineness) relationship on topologies. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ) β§ π½ β πΎ) β (πGenβπ½) β (πGenβπΎ)) | ||
Theorem | kgencn 23059* | A function from a compactly generated space is continuous iff it is continuous "on compacta". (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β ((πGenβπ½) Cn πΎ) β (πΉ:πβΆπ β§ βπ β π« π((π½ βΎt π) β Comp β (πΉ βΎ π) β ((π½ βΎt π) Cn πΎ))))) | ||
Theorem | kgencn2 23060* | A function πΉ:π½βΆπΎ from a compactly generated space is continuous iff for all compact spaces π§ and continuous π:π§βΆπ½, the composite πΉ β π:π§βΆπΎ is continuous. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β (TopOnβπ) β§ πΎ β (TopOnβπ)) β (πΉ β ((πGenβπ½) Cn πΎ) β (πΉ:πβΆπ β§ βπ§ β Comp βπ β (π§ Cn π½)(πΉ β π) β (π§ Cn πΎ)))) | ||
Theorem | kgencn3 23061 | The set of continuous functions from π½ to πΎ is unaffected by k-ification of πΎ, if π½ is already compactly generated. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ ((π½ β ran πGen β§ πΎ β Top) β (π½ Cn πΎ) = (π½ Cn (πGenβπΎ))) | ||
Theorem | kgen2cn 23062 | A continuous function is also continuous with the domain and codomain replaced by their compact generator topologies. (Contributed by Mario Carneiro, 21-Mar-2015.) |
β’ (πΉ β (π½ Cn πΎ) β πΉ β ((πGenβπ½) Cn (πGenβπΎ))) | ||
Syntax | ctx 23063 | Extend class notation with the binary topological product operation. |
class Γt | ||
Syntax | cxko 23064 | Extend class notation with a function whose value is the compact-open topology. |
class βko | ||
Definition | df-tx 23065* | Define the binary topological product, which is homeomorphic to the general topological product over a two element set, but is more convenient to use. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ Γt = (π β V, π β V β¦ (topGenβran (π₯ β π, π¦ β π β¦ (π₯ Γ π¦)))) | ||
Definition | df-xko 23066* | Define the compact-open topology, which is the natural topology on the set of continuous functions between two topological spaces. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ βko = (π β Top, π β Top β¦ (topGenβ(fiβran (π β {π₯ β π« βͺ π β£ (π βΎt π₯) β Comp}, π£ β π β¦ {π β (π Cn π ) β£ (π β π) β π£})))) | ||
Theorem | txval 23067* | Value of the binary topological product operation. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 30-Aug-2015.) |
β’ π΅ = ran (π₯ β π , π¦ β π β¦ (π₯ Γ π¦)) β β’ ((π β π β§ π β π) β (π Γt π) = (topGenβπ΅)) | ||
Theorem | txuni2 23068* | The underlying set of the product of two topologies. (Contributed by Mario Carneiro, 31-Aug-2015.) |
β’ π΅ = ran (π₯ β π , π¦ β π β¦ (π₯ Γ π¦)) & β’ π = βͺ π & β’ π = βͺ π β β’ (π Γ π) = βͺ π΅ | ||
Theorem | txbasex 23069* | The basis for the product topology is a set. (Contributed by Mario Carneiro, 2-Sep-2015.) |
β’ π΅ = ran (π₯ β π , π¦ β π β¦ (π₯ Γ π¦)) β β’ ((π β π β§ π β π) β π΅ β V) | ||
Theorem | txbas 23070* | The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 31-Aug-2015.) |
β’ π΅ = ran (π₯ β π , π¦ β π β¦ (π₯ Γ π¦)) β β’ ((π β TopBases β§ π β TopBases) β π΅ β TopBases) | ||
Theorem | eltx 23071* | A set in a product is open iff each point is surrounded by an open rectangle. (Contributed by Stefan O'Rear, 25-Jan-2015.) |
β’ ((π½ β π β§ πΎ β π) β (π β (π½ Γt πΎ) β βπ β π βπ₯ β π½ βπ¦ β πΎ (π β (π₯ Γ π¦) β§ (π₯ Γ π¦) β π))) | ||
Theorem | txtop 23072 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ ((π β Top β§ π β Top) β (π Γt π) β Top) | ||
Theorem | ptval 23073* | The value of the product topology function. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ Fn π΄) β (βtβπΉ) = (topGenβπ΅)) | ||
Theorem | ptpjpre1 23074* | The preimage of a projection function can be expressed as an indexed cartesian product. (Contributed by Mario Carneiro, 6-Feb-2015.) |
β’ π = Xπ β π΄ βͺ (πΉβπ) β β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (β‘(π€ β π β¦ (π€βπΌ)) β π) = Xπ β π΄ if(π = πΌ, π, βͺ (πΉβπ))) | ||
Theorem | elpt 23075* | Elementhood in the bases of a product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ (π β π΅ β ββ((β Fn π΄ β§ βπ¦ β π΄ (ββπ¦) β (πΉβπ¦) β§ βπ€ β Fin βπ¦ β (π΄ β π€)(ββπ¦) = βͺ (πΉβπ¦)) β§ π = Xπ¦ β π΄ (ββπ¦))) | ||
Theorem | elptr 23076* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ (πΊ Fn π΄ β§ βπ¦ β π΄ (πΊβπ¦) β (πΉβπ¦)) β§ (π β Fin β§ βπ¦ β (π΄ β π)(πΊβπ¦) = βͺ (πΉβπ¦))) β Xπ¦ β π΄ (πΊβπ¦) β π΅) | ||
Theorem | elptr2 23077* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} & β’ (π β π΄ β π) & β’ (π β π β Fin) & β’ ((π β§ π β π΄) β π β (πΉβπ)) & β’ ((π β§ π β (π΄ β π)) β π = βͺ (πΉβπ)) β β’ (π β Xπ β π΄ π β π΅) | ||
Theorem | ptbasid 23078* | The base set of the product topology is a basic open set. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ β π΄ βͺ (πΉβπ) β π΅) | ||
Theorem | ptuni2 23079* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ β π΄ βͺ (πΉβπ) = βͺ π΅) | ||
Theorem | ptbasin 23080* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (π β π΅ β§ π β π΅)) β (π β© π) β π΅) | ||
Theorem | ptbasin2 23081* | The basis for a product topology is closed under intersections. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β (fiβπ΅) = π΅) | ||
Theorem | ptbas 23082* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β π΅ β TopBases) | ||
Theorem | ptpjpre2 23083* | The basis for a product topology is a basis. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π΅ = {π₯ β£ βπ((π Fn π΄ β§ βπ¦ β π΄ (πβπ¦) β (πΉβπ¦) β§ βπ§ β Fin βπ¦ β (π΄ β π§)(πβπ¦) = βͺ (πΉβπ¦)) β§ π₯ = Xπ¦ β π΄ (πβπ¦))} & β’ π = Xπ β π΄ βͺ (πΉβπ) β β’ (((π΄ β π β§ πΉ:π΄βΆTop) β§ (πΌ β π΄ β§ π β (πΉβπΌ))) β (β‘(π€ β π β¦ (π€βπΌ)) β π) β π΅) | ||
Theorem | ptbasfi 23084* | 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 23085 | The product topology is a topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ ((π΄ β π β§ πΉ:π΄βΆTop) β (βtβπΉ) β Top) | ||
Theorem | ptopn 23086* | A basic open set in the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆTop) & β’ (π β π β Fin) & β’ ((π β§ π β π΄) β π β (πΉβπ)) & β’ ((π β§ π β (π΄ β π)) β π = βͺ (πΉβπ)) β β’ (π β Xπ β π΄ π β (βtβπΉ)) | ||
Theorem | ptopn2 23087* | A sub-basic open set in the product topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ (π β π΄ β π) & β’ (π β πΉ:π΄βΆTop) & β’ (π β π β (πΉβπ)) β β’ (π β Xπ β π΄ if(π = π, π, βͺ (πΉβπ)) β (βtβπΉ)) | ||
Theorem | xkotf 23088* | Functionality of function π. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π & β’ πΎ = {π₯ β π« π β£ (π βΎt π₯) β Comp} & β’ π = (π β πΎ, π£ β π β¦ {π β (π Cn π) β£ (π β π) β π£}) β β’ π:(πΎ Γ π)βΆπ« (π Cn π) | ||
Theorem | xkobval 23089* | 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 23090* | Value of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π & β’ πΎ = {π₯ β π« π β£ (π βΎt π₯) β Comp} & β’ π = (π β πΎ, π£ β π β¦ {π β (π Cn π) β£ (π β π) β π£}) β β’ ((π β Top β§ π β Top) β (π βko π ) = (topGenβ(fiβran π))) | ||
Theorem | xkotop 23091 | The compact-open topology is a topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ ((π β Top β§ π β Top) β (π βko π ) β Top) | ||
Theorem | xkoopn 23092* | A basic open set of the compact-open topology. (Contributed by Mario Carneiro, 19-Mar-2015.) |
β’ π = βͺ π & β’ (π β π β Top) & β’ (π β π β Top) & β’ (π β π΄ β π) & β’ (π β (π βΎt π΄) β Comp) & β’ (π β π β π) β β’ (π β {π β (π Cn π) β£ (π β π΄) β π} β (π βko π )) | ||
Theorem | txtopi 23093 | The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ π β Top & β’ π β Top β β’ (π Γt π) β Top | ||
Theorem | txtopon 23094 | 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 23095 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 2-Sep-2009.) |
β’ π = βͺ π & β’ π = βͺ π β β’ ((π β Top β§ π β Top) β (π Γ π) = βͺ (π Γt π)) | ||
Theorem | txunii 23096 | The underlying set of the product of two topologies. (Contributed by Jeff Madsen, 15-Jun-2010.) |
β’ π β Top & β’ π β Top & β’ π = βͺ π & β’ π = βͺ π β β’ (π Γ π) = βͺ (π Γt π) | ||
Theorem | ptuni 23097* | The base set for the product topology. (Contributed by Mario Carneiro, 3-Feb-2015.) |
β’ π½ = (βtβπΉ) β β’ ((π΄ β π β§ πΉ:π΄βΆTop) β Xπ₯ β π΄ βͺ (πΉβπ₯) = βͺ π½) | ||
Theorem | ptunimpt 23098* | Base set of a product topology given by substitution. (Contributed by Stefan O'Rear, 22-Feb-2015.) |
β’ π½ = (βtβ(π₯ β π΄ β¦ πΎ)) β β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β Top) β Xπ₯ β π΄ βͺ πΎ = βͺ π½) | ||
Theorem | pttopon 23099* | The base set for the product topology. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ π½ = (βtβ(π₯ β π΄ β¦ πΎ)) β β’ ((π΄ β π β§ βπ₯ β π΄ πΎ β (TopOnβπ΅)) β π½ β (TopOnβXπ₯ β π΄ π΅)) | ||
Theorem | pttoponconst 23100 | The base set for a product topology when all factors are the same. (Contributed by Mario Carneiro, 22-Aug-2015.) |
β’ π½ = (βtβ(π΄ Γ {π })) β β’ ((π΄ β π β§ π β (TopOnβπ)) β π½ β (TopOnβ(π βm π΄))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |