TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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.

A product of connected spaces is connected in the product topology, and that argument is a theorem of ZF; for an infinite index set it is the assertion that the product of nonempty spaces is nonempty that uses the Axiom of Choice

Statement

Let $I$ be a set, let $(X_{i}, T_{i})$ be a connected topological space (Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets) for each $i \in I$ , and give $P : = \prod_{i \in 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 $P$ is connected.

The choice cost, stated exactly. The proof needs one point $a \in P$ and nothing else, and it obtains it as follows.

If $P = \emptyset$ then $P$ is connected outright, no separation of the empty space existing, and no choice principle is involved.
If $P \neq \emptyset$ a point $a \in P$ is fixed. Selecting one element of one nonempty set is not a choice principle.

So the theorem as displayed is a theorem of ZF. What costs something is the companion assertion that $P$ is nonempty when every $X_{i}$ is: for $I$ a natural number that is Every natural-number-indexed list of nonempty sets has a choice function on its family of values, a theorem of ZF, and for an arbitrary $I$ it is the Axiom of Choice (The Axiom of Choice, Choice function), as 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 records. A reader who wants "the product of nonempty connected spaces is a nonempty connected space" for infinite $I$ is therefore using $A C$ , and that is where the cost sits — not in the connectedness argument.

Facts & Assumptions

Given: A set $I$ , connected spaces $(X_{i})_{i \in I}$ , and $P = \prod_{i \in I} X_{i}$ with the product topology and projections $π_{i}$ .

[A1]

A point of $P$ is a function $x$ on $I$ with $x_{i} \in X_{i}$ for every $i$ ; the sets $\prod_{i} U_{i}$ with $U_{i}$ open and $U_{i} = X_{i}$ for all but finitely many $i$ form a basis of 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, Basis and subbasis for a topology, and the topology generated by a family of sets).

[A2]

A map $h : Z \to P$ is continuous exactly when every component $π_{i} \circ h$ is continuous; constant maps are continuous, a preimage under a constant map being $\emptyset$ or $Z$ (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, claim 2, Continuity of a map of topological spaces at a point and globally).

[A3]

A continuous image of a connected space is a connected subset of the target (A continuous image of a connected space is connected, and connectedness is a topological property, claim 1).

[A4]

A union of connected subsets each meeting a fixed connected subset $A$ , together with $A$ , is connected; a union of connected subsets with a common point is connected; a singleton is connected (A union of connected subspaces with a point in common is connected, and so is a union of a family in which every member meets a fixed connected member, claims 1 and 2, Separation of a topological space, connected and disconnected spaces, clopen sets, and connected subsets).

[A5]

If $A$ is connected and $A \subseteq B \subseteq \overline{A}$ then $B$ is connected; $D \subseteq P$ is dense exactly when it meets every nonempty basic open set, and then $\overline{D} = P$ (If $A$ is connected and $A \subseteq B \subseteq \overline{A}$ then $B$ is connected; in particular the closure of a connected set is connected, Dense, nowhere dense and codense subsets of a topological space, and the criterion by basic open sets, 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, Interior, closure, boundary, exterior, derived set and isolated point in a topological space, 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).

[A6]

Induction on $N$ : a property holding at $0$ and passing from $n$ to $n + 1$ holds at every natural number (The principle of mathematical induction). A set $F$ is finite exactly when $F \approx n$ for some $n \in N$ , that is exactly when some bijection $n \to F$ exists (Finite, countably infinite, countable, uncountable).

Proof

technique · direct

1.1

If $P = \emptyset$ then $P$ is connected, no separation of the empty space existing, and the theorem holds; so assume $P \neq \emptyset$ and fix a single point $a \in P$ .

A4given

1.2

For a function $σ$ with domain a natural number $n$ and values in $I$ , put $P_{σ} : = {x \in P : x_{j} = a_{j} for every j \in I ∖ σ [n]}$ , the points agreeing with $a$ outside the finite set $σ [n]$ .

A1given

1.3

For $x \in P$ and $i \in I$ let $T_{x, i} : = {y \in P : y_{j} = x_{j} for every j \neq i}$ , the $i$ -th axis through $x$ ; the map $t_{x, i} : X_{i} \to P$ sending $u$ to the point with $i$ -th coordinate $u$ and $j$ -th coordinate $x_{j}$ for $j \neq i$ has image $T_{x, i}$ .

2.1

Each $t_{x, i}$ is continuous, since its $i$ -th component is the identity of $X_{i}$ and its $j$ -th component for $j \neq i$ is constant, so [A2] applies; hence $T_{x, i}$ is a connected subset of $P$ by [A3], $X_{i}$ being connected.

step 1.3A2A3

2.2

By induction on $n \in N$ using [A6]: for every function $σ$ with domain $n$ and values in $I$ , the set $P_{σ}$ is connected. At $n = 0$ the domain is empty, $σ [0] = \emptyset$ , and $P_{σ} = {a}$ , a singleton, connected by [A4].

step 1.1step 1.2A4A6

2.3

For the step, let $σ$ have domain $n + 1$ , let $τ : = σ ∣_{n}$ and let $i : = σ (n)$ ; then $σ [n + 1] = τ [n] \cup {i}$ , so $P_{τ} \subseteq P_{σ}$ and every $T_{x, i}$ with $x \in P_{τ}$ is contained in $P_{σ}$ , since a point of it agrees with $x$ , hence with $a$ , off $τ [n] \cup {i}$ .

step 1.2step 1.3

2.4

Moreover $P_{σ} = P_{τ} \cup ⋃_{x \in P_{τ}} T_{x, i}$ : given $y \in P_{σ}$ , the point $x$ obtained from $y$ by resetting the $i$ -th coordinate to $a_{i}$ lies in $P_{τ}$ , and $y \in T_{x, i}$ .

step 1.2step 1.3

3.1

So, assuming inductively that $P_{τ}$ is connected, each $T_{x, i}$ with $x \in P_{τ}$ is connected by step 2.1 and meets $P_{τ}$ in $x$ , whence $P_{σ}$ is connected by [A4] and step 2.4; by [A6] this proves the claim of step 2.2 for every $n$ .

step 2.1step 2.2step 2.3step 2.4A4A6

4.1

Let $D : = ⋃ {P_{σ} : σ a function from a natural number into I}$ , the set of points of $P$ agreeing with $a$ outside a finite subset of $I$ ; every $P_{σ}$ is connected by step 3.1 and contains $a$ , so $D$ is connected by [A4].

step 3.1A4

5.1

$D$ is dense in $P$ : let $B = \prod_{i} U_{i}$ be a nonempty basic open set as in [A1], with $U_{i} = X_{i}$ off a finite $F \subseteq I$ , and fix $y \in B$ ; write $F = σ [n]$ for a bijection $σ : n \to F$ , which exists by [A6]; the point $x$ with $x_{j} : = y_{j}$ for $j \in F$ and $x_{j} : = a_{j}$ otherwise lies in $P_{σ} \subseteq D$ , and lies in $B$ , since $x_{j} = y_{j} \in U_{j}$ for $j \in F$ and $x_{j} \in X_{j} = U_{j}$ otherwise.

step 1.2step 4.1A1A6

6.1

Hence $\overline{D} = P$ by [A5], and $D \subseteq P \subseteq \overline{D}$ , so $P$ is connected by [A5] and step 4.1.

step 4.1step 5.1A5∎

Remarks

Why the finite-support points and not the whole product at once. A basic open set of the product topology constrains only finitely many coordinates, so a point that has been moved away from $a$ in finitely many coordinates is already enough to meet every basic open set. That is the entire reason the theorem is true for arbitrary $I$ , and it is also why the same argument fails for the box topology, where a basic open set may constrain every coordinate at once, so a point moved in finitely many coordinates need not meet it.
The induction is on the number of moved coordinates, not on $I$ . Step 3.1 runs over $n \in N$ and quantifies over all functions from $n$ into $I$ , so no ordering or enumeration of $I$ is needed and $I$ may have any cardinality whatever.
Where a choice principle would enter if the statement were strengthened. The proof selects a single point $a$ and, in step 6.1, a single point $y$ of a nonempty set — one selection each, not a family of them. What cannot be done in ZF for infinite $I$ is to produce a point of $P$ from the mere nonemptiness of every factor; that assertion is $A C$ itself (The Axiom of Choice), and it is the reason the Statement above separates connectedness from nonemptiness rather than bundling them.

Depends on

Used by

Dependency tree · two levels

42 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Connected space (Wikipedia) (standard reference, not scraped)
Product topology (Wikipedia) (standard reference, not scraped)
Paul Bankston, Metric Topology: A First Course (standard reference, not scraped)
General topology (Wikipedia) (standard reference, not scraped)