TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Products commute with subspaces; for infinite nonempty families, the closure identity $\overline{\prod A_i}=\prod \overline{A_i}$ uses the Axiom of Choice

Statement

Let $(X_i, \mathcal{T}_i)_{i \in I}$ be topological spaces, let $A_i \subseteq X_i$ for each $i$ , and give $\prod_{i} X_i$ the product topology (The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space). Then:

Subspaces commute with products. The product of the subspace topologies on the $A_i$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace) is exactly the subspace topology that $\prod_i A_i$ inherits from $\prod_i X_i$ . So the phrase "the product of the subspaces $A_i$ " names one topology, whichever of the two routes is taken.
Closure of a product is the product of the closures. In $\prod_i X_i$ , $\overline{\prod_{i \in I} A_i} \;=\; \prod_{i \in I} \overline{A_i} ,$ closures being taken in $\prod_i X_i$ and in $X_i$ respectively (Interior, closure, boundary, exterior, derived set and isolated point in a topological space). In particular $\prod_i A_i$ is closed in the product whenever every $A_i$ is closed in $X_i$ .

No hypothesis of nonemptiness is imposed in claim 2: if some $A_{i_0}$ is empty then both sides are empty, since $\overline{\varnothing} = \varnothing$ . When every $A_i$ is nonempty the inclusion $\supseteq$ of claim 2 uses the Axiom of Choice for infinite $I$ (The Axiom of Choice) and Every natural-number-indexed list of nonempty sets has a choice function on its family of values for $I$ a natural number, and that is the only place in the item where a choice principle appears.

Facts & Assumptions

Given: Topological spaces $(X_i,\mathcal{T}_i)_{i \in I}$ , subsets $A_i \subseteq X_i$ , the product $P := \prod_i X_i$ with the product topology, the subset $A := \prod_i A_i \subseteq P$ , and the projections $\pi_j : P \to X_j$ and $\pi^A_j : A \to A_j$ .

[A1]

A basis for the product topology on $P$ is the family of boxes $\prod_i U_i$ with every $U_i$ open and $U_i = X_i$ off a set listed as $\{i_0,\dots,i_{n-1}\}$ for some natural $n$ ; the product topology is generated by the subbasis $\{\pi_i^{-1}[U] : U \in \mathcal{T}_i\}$ (The product set $\prod_{i \in I} X_i$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A family is a basis for a unique topology iff it covers the set and every point of an intersection of two members lies in a member inside that intersection; finite intersections of any subbasis form a basis).

[A2]

The subspace topology on $A \subseteq P$ is $\{\, O \cap A : O \text{ open in } P \,\}$ , and likewise on each $A_i \subseteq X_i$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace).

[L1]

A topology generated by a family is the coarsest topology containing it, and two families generating the same topology may be exchanged freely (Basis and subbasis for a topology, and the topology generated by a family of sets).

[L2]

The projections $\pi_j$ are continuous, and a map into a product is continuous exactly when all its components are (A map into a product is continuous iff each of its components is; the projections are continuous and open; and each projection is surjective when every factor is nonempty, which for an infinite index set uses the Axiom of Choice, Characteristic properties: a map into a space with the initial topology is continuous iff every composite with the defining family is, a map out of a space with the final topology is continuous iff every composite with the defining family is, and the two topologies are respectively the coarsest and the finest making that family continuous).

[L3]

For a continuous $f$ one has $f[\overline{B}] \subseteq \overline{f[B]}$ for every subset $B$ of the source (For a map of spaces the following agree: continuity at every point, preimages of open sets open, preimages of closed sets closed, preimages of subbasic open sets open, and $f(\overline{A}) \subseteq \overline{f(A)}$ , clause (e)).

[L4]

$x \in \overline{B}$ if and only if every basic open set containing $x$ meets $B$ ; $\overline{B}$ is the smallest closed superset of $B$ , and $\overline{\varnothing} = \varnothing$ (A point lies in the closure of $A$ iff every basic neighbourhood of it meets $A$ ; the closure is the smallest closed superset and equals $A$ together with its derived set, clauses (c) and (d) and claim 2; Interior, closure, boundary, exterior, derived set and isolated point in a topological space).

[L5]

A function on a natural number $n$ whose values are nonempty sets has a choice function for its family of values (Every natural-number-indexed list of nonempty sets has a choice function on its family of values, Choice function); a family of nonempty sets indexed by an arbitrary set has one by the Axiom of Choice (The Axiom of Choice).

Proof

technique · direct

1.1

For $i \in I$ and $U \in \mathcal{T}_i$ one has $(\pi^A_i)^{-1}[U \cap A_i] = \{\, x \in A : x_i \in U \cap A_i \,\} = \{\, x \in A : x_i \in U \,\} = \pi_i^{-1}[U] \cap A$ , the middle equality holding because every $x \in A$ already satisfies $x_i \in A_i$ .

givenA2

1.2

As $U$ ranges over $\mathcal{T}_i$ and $i$ over $I$ , the sets $\pi_i^{-1}[U] \cap A$ are exactly the traces on $A$ of the subbasic open sets of $P$ , and the sets $U \cap A_i$ are exactly the open sets of the subspace $A_i$ .

A1A2

1.3

If some $A_{i_0} = \varnothing$ then $A = \varnothing$ and $\overline{A_{i_0}} = \varnothing$ by [L4], so $\overline{A} = \varnothing$ and $\prod_i \overline{A_i} = \varnothing$ as well.

givenL4

1.4

Each $\pi_i$ is continuous and $\pi_i[A] \subseteq A_i$ , so [L3] gives $\pi_i[\overline{A}] \subseteq \overline{\pi_i[A]} \subseteq \overline{A_i}$ ; hence every $x \in \overline{A}$ has $x_i \in \overline{A_i}$ for every $i$ , that is $\overline{A} \subseteq \prod_i \overline{A_i}$ .

givenL2L3L4

1.5

Assume every $A_i$ is nonempty, and fix by [L5] a point $a \in \prod_i A_i = A$ .

L5choose

1.6

Assume every $A_i$ is nonempty, let $x \in \prod_i \overline{A_i}$ and let $B = \prod_i O_i$ be a basic open set of $P$ with $x \in B$ , with $O_i = X_i$ off $\{i_0,\dots,i_{n-1}\}$ as in [A1]. For each $m < n$ the set $O_{i_m} \cap A_{i_m}$ is nonempty, since $x_{i_m} \in \overline{A_{i_m}}$ and $O_{i_m}$ is an open set containing it.

A1L4

2.1

By step 1.1 and step 1.2 the initial topology on $A$ of the family $(\pi^A_i)$ and the subspace topology on $A$ are generated by the same family of subsets of $A$ : the first by the sets $(\pi^A_i)^{-1}[W]$ with $W$ open in $A_i$ , the second by the traces on $A$ of the open sets of $P$ , whose subbasic members are the traces of the sets $\pi_i^{-1}[U]$ . So the two topologies coincide, which is claim 1.

step 1.1step 1.2A1A2L1

2.2

By [L5] applied to the function $m \mapsto O_{i_m} \cap A_{i_m}$ on $n$ , choose $c_m \in O_{i_m} \cap A_{i_m}$ for each $m < n$ , and define $y \in P$ by $y_{i_m} := c_m$ for $m < n$ and $y_i := a_i$ for every other $i$ , with $a$ as in step 1.5. Then $y_i \in A_i$ for every $i$ , so $y \in A$ ; and $y_i \in O_i$ for every $i$ , since $O_i = X_i$ off the listed indices. So $y \in B \cap A$ .

step 1.5step 1.6L5choose

3.1

By step 2.2 every basic open set containing $x$ meets $A$ , so $x \in \overline{A}$ by [L4]; hence $\prod_i \overline{A_i} \subseteq \overline{A}$ when every $A_i$ is nonempty, and with step 1.4 the two sets are equal in that case.

step 1.4step 2.2L4

4.1

Step 1.3 disposes of the case in which some $A_i$ is empty and step 3.1 of the case in which none is, so claim 2 holds in general; the final sentence of claim 2 follows because $A_i = \overline{A_i}$ for every $i$ then gives $\overline{A} = A$ , which is closedness by [L4]. With step 2.1 both claims are proved.

step 1.3step 2.1step 3.1L4∎

Remarks

Claim 1 is what lets " $\prod A_i$ " be written without a warning. Every later item that forms a product of subspaces, the Hilbert cube and the Cantor set among them, silently uses it: the topology on $[0,1]^{\mathbb{N}}$ obtained by taking the product of the subspaces $[0,1] \subseteq \mathbb{R}$ is the topology it inherits as a subset of $\mathbb{R}^{\mathbb{N}}$ .
Claim 2 fails for the box topology in the direction one might expect it to hold. Nothing above is claimed for $\mathcal{T}^{\square}$ . The inclusion $\overline{A} \subseteq \prod \overline{A_i}$ survives there without any choice principle, since it uses only continuity of the projections, which holds for the box topology as well. The reverse inclusion also holds for the box topology, but only with the Axiom of Choice (The Axiom of Choice): given $x \in \prod \overline{A_i}$ and a box $\prod_i U_i$ around $x$ , every $U_i \cap A_i$ is nonempty, and a choice function picks a point of $\bigl(\prod_i U_i\bigr) \cap \prod_i A_i$ . What is genuinely not claimed here is a choice-free proof of that half.
The choice is spent on the coordinates that the basic open set leaves unrestricted. Those are all but finitely many, and for each of them the point $y$ of step 2.2 needs some member of $A_i$ ; the finitely many restricted coordinates are handled by Every natural-number-indexed list of nonempty sets has a choice function on its family of values alone. That split is exactly why the finite case of claim 2 is a theorem of ZF.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 53 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Product topology (Wikipedia) (standard reference, not scraped)
Subspace topology (Wikipedia) (standard reference, not scraped)
J. Munkres, Topology, 2nd ed., §19 (standard reference, not scraped)

Products commute with subspaces; for infinite nonempty families, the closure identity ∏Ai‾=∏Ai‾\overline{\prod A_i}=\prod \overline{A_i}∏Ai​​=∏Ai​​ uses the Axiom of Choice