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 [7] and [6], not even by Bourbaki in [4].

Let {T_i}_i∈I be a family of topological spaces. The prebasis of the product space T = ∏_i∈I T_i is defined in [5] as the set of all π⁻¹_i(V) with i ∈ I and V open in T_i. Here it is shown that the basis generated by this prebasis consists exactly of the sets ∏_i∈I V_i with V_i open in T_i and for all but finitely many i ∈ I holds V_i = T_i. Given I = {a} we have T ≅ T_a, given I = {a, b} with a≠ b we have T ≅ T_a ×T_b. Given another family of topological spaces {S_i}_i∈I such that S_i ≅ T_i for all i ∈ I, we have S = ∏_i∈I S_i ≅ T. If instead S_i is a subspace of T_i 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].