<abstract xmlns="http://www.w3.org/1999/xhtml">This article covers some technical aspects about the product topology which are usually not given much of a thought in mathematics and standard literature like [7] and [6], not even by Bourbaki in [4].Let <italic>{Ti}i∈I</italic> be a family of topological spaces. The prebasis of the product space <italic>T</italic> = ∏<italic>i∈I Ti</italic> is defined in [5] as the set of all <italic>π</italic>−1<italic>i</italic>(<italic>V</italic>) with <italic>i ∈ I</italic> and <italic>V</italic> open in <italic>Ti</italic>. Here it is shown that the basis generated by this prebasis consists exactly of the sets ∏<italic>i∈I Vi</italic> with <italic>Vi</italic> open in <italic>Ti</italic> and for all but finitely many <italic>i ∈ I</italic> holds <italic>Vi</italic> = <italic>Ti</italic>. Given <italic>I</italic> = <italic>{a}</italic> we have <italic>T</italic> ≅ <italic>Ta</italic>, given <italic>I</italic> = <italic>{a, b}</italic> with <italic>a</italic>≠ <italic>b</italic> we have <italic>T</italic> ≅ <italic>Ta ×Tb</italic>. Given another family of topological spaces <italic>{Si}i∈I</italic> such that <italic>Si</italic> ≅ <italic>Ti</italic> for all <italic>i ∈ I</italic>, we have <italic>S</italic> = ∏<italic>i∈I Si</italic> ≅ <italic>T</italic>. If instead <italic>Si</italic> is a subspace of <italic>Ti</italic> for each <italic>i ∈ I</italic>, then <italic>S</italic> is a subspace of <italic>T</italic>.These results are obvious for mathematicians, but formally proven here by means of the Mizar system [3], [2].</abstract>

This article covers some technical aspects about the product topology which are usually not given much of a thought in mathematics and standard literature like [7] and [6], not even by Bourbaki in [4].Let {Ti}i∈I be a family of topological spaces. The prebasis of the product space T = ∏i∈I Ti is defined in [5] as the set of all π−1i(V) with i ∈ I and V open in Ti. Here it is shown that the basis generated by this prebasis consists exactly of the sets ∏i∈I Vi with Vi open in Ti and for all but finitely many i ∈ I holds Vi = Ti. Given I = {a} we have T ≅ Ta, given I = {a, b} with a≠ b we have T ≅ Ta ×Tb. Given another family of topological spaces {Si}i∈I such that Si ≅ Ti for all i ∈ I, we have S = ∏i∈I Si ≅ T. If instead Si is a subspace of Ti for each i ∈ I, then S is a subspace of T.These results are obvious for mathematicians, but formally proven here by means of the Mizar system [3], [2].

Some Remarks about Product Spaces

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

{"article-title":"Some Remarks about Product Spaces"}

This article covers some technical aspects about the product topology which are usually not given much of a thought in mathematics and standard literature like...

Some Remarks about Product Spaces

Online veröffentlicht: 23. Feb. 2019

Seitenbereich: 209 - 222

Akzeptiert: 29. Sept. 2018

DOI: https://doi.org/10.2478/forma-2018-0019

Schlüsselwörter
topology, product spaces

© 2018 Sebastian Koch, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Some Remarks about Product Spaces

Online veröffentlicht: 23. Feb. 2019

Seitenbereich: 209 - 222

Akzeptiert: 29. Sept. 2018

DOI: https://doi.org/10.2478/forma-2018-0019

Schlüsselwörtertopology, product spaces

© 2018 Sebastian Koch, published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 3.0 License.

Schlüsselwörter
topology, product spaces