ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

The Hilbert cube $[0, 1]^{N}$ with the product topology is metrizable, by $d (x, y) = \sum_{k} ∣ x_{k} - y_{k} ∣ / 2^{k + 1}$

Example

Let $[0, 1]$ carry the subspace topology from the usual topology of $R$ (Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length, 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, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded) and let

$Q : = [0, 1]^{N} = \prod_{k \in N} [0, 1]$

carry 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); $Q$ is the Hilbert cube. Define

$d (x, y) : = \sum_{k = 0}^{\infty} \frac{∣ x_{k} - y_{k} ∣}{2^{k + 1}} (x, y \in Q) .$

Then:

$d$ is defined, with $0 \leq d (x, y) \leq 1$ : the series has nonnegative terms bounded by $2^{- (k + 1)}$ , and $\sum_{k} 2^{- (k + 1)} = 1$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges, If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ).
$d$ is a metric on $Q$ (Metric space: $d (x, y) = 0$ iff $x = y$ , symmetry, and the triangle inequality; pseudometric and ultrametric).
$d$ induces the product topology, so $Q$ is metrizable (Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not).

Claim 3 is the only real work, and it is what the index weights are for: the factor $2^{- (k + 1)}$ makes the tail of the sum small no matter what the coordinates do, so a constraint on finitely many coordinates already forces $d$ to be small, and conversely $d$ small forces each individual coordinate to be close.

By claim 1 of Products commute with subspaces; for infinite nonempty families, the closure identity $\overline{\prod A_{i}} = \prod \overline{A_{i}}$ uses the Axiom of Choice the topology on $Q$ is also the subspace topology it inherits from $R^{N}$ , so the two readings of " $[0, 1]^{N}$ " agree.

Facts & Assumptions

Given: $Q = \prod_{k \in N} [0, 1]$ with the product topology, points $x, y, z \in Q$ , the function $d$ above, and a real $r > 0$ . Powers $2^{- k}$ are integer powers (Integer powers $a^{m}$ ) and $2$ denotes $ι (2)$ (The canonical natural $ι (n) = n \cdot 1_{F}$ of a field).

[A1]

A basis for the product topology on $Q$ is the family of boxes $\prod_{k} O_{k}$ with every $O_{k}$ open in $[0, 1]$ and $O_{k} = [0, 1]$ off a list $k_{0}, \dots, k_{n - 1}$ ; the product topology is generated by the sets $π_{j}^{- 1} [O]$ with $O$ open in $[0, 1]$ (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).

[A2]

$O \subseteq [0, 1]$ is open in $[0, 1]$ exactly when $O = V \cap [0, 1]$ for some $V$ open in $R$ ; in particular ${t \in [0, 1] : ∣ t - s ∣ < ε} = (s - ε, s + ε) \cap [0, 1]$ is open in $[0, 1]$ for every $s$ and every $ε > 0$ , and every open $O ∋ s$ of $[0, 1]$ contains such a set (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, The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded, Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length).

[L1]

$\sum_{k = 0}^{\infty} r^{k} = 1 / (1 - r)$ for $∣ r ∣ < 1$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges); a nonnegative series converges iff its partial sums are bounded, and then each partial sum is at most the sum (A series of nonnegative terms converges iff its partial sums are bounded, and then the sum is their supremum); a nonnegative series dominated termwise by a convergent one converges (If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ ); series are additive and homogeneous (Convergent series add and scale termwise, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L2]

Finite sums are monotone in their terms, $\sum_{k < n} λ = n λ$ , and a finite sum of nonnegative terms that vanishes has all its terms zero (Laws of finite sums and finite products, claims 2 and 4); weak inequalities pass to limits (Limits preserve non-strict inequalities).

[L3]

$∣ s ∣ \geq 0$ , $∣ s ∣ = 0$ iff $s = 0$ , $∣ s ∣ = ∣ - s ∣$ (Basic properties of the absolute value), and $∣ s - u ∣ \leq ∣ s - t ∣ + ∣ t - u ∣$ (The triangle inequality).

[L4]

$2^{m} 2^{n} = 2^{m + n}$ and $2^{- m} = (2^{m})^{- 1}$ , with $2^{k} > 0$ (Laws of integer exponents, Integer powers $a^{m}$ , Inverses of positives are positive, and reciprocation reverses order).

[L5]

If $\sum a_{k}$ converges then $a_{k} \to 0$ (If a series converges then its terms tend to $0$ ); below any positive real lies a positive rational (The rationals embed densely in the reals), so a convergence tested at rational tolerances delivers every real tolerance.

[L6]

In a metric space the balls $B_{d} (u, ρ)$ form a basis of the metric topology, and $U$ is $d$ -open exactly when every $u \in U$ has some $ρ > 0$ with $B_{d} (u, ρ) \subseteq U$ (The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement, Open ball, closed ball and sphere in a metric space).

Verification

technique · direct

1.1

$\sum_{k} 2^{- (k + 1)} = 1$ , being $\frac{1}{2} \sum_{k} 2^{- k} = \frac{1}{2} \cdot 2$ by [L1] and [L4]; and more generally $\sum_{k \geq N} 2^{- (k + 1)} = 2^{- N}$ for every $N \in N$ , by shifting the index.

L1L4

1.2

$2^{- k} \to 0$ , since $\sum_{k} 2^{- k}$ converges by [L1]; so for every real $η > 0$ there is $N \in N$ with $2^{- N} < η$ .

L1L5

1.3

$d (x, y) = d (y, x)$ , term by term, by [L3]. This is (M2).

2.1

For $x, y \in Q$ and every $k$ : $0 \leq ∣ x_{k} - y_{k} ∣ \leq 1$ , since both coordinates lie in $[0, 1]$ ; hence $0 \leq ∣ x_{k} - y_{k} ∣ 2^{- (k + 1)} \leq 2^{- (k + 1)}$ . By [L1] and step 1.1 the series defining $d (x, y)$ converges and $0 \leq d (x, y) \leq 1$ . This is claim 1.

step 1.1A2L1L2L3L4

3.1

For every $j \in N$ and $x, y \in Q$ : $∣ x_{j} - y_{j} ∣ 2^{- (j + 1)} \leq d (x, y)$ , the left side being a single term of a nonnegative convergent series and hence at most one of its partial sums, which is at most the sum by [L1].

step 2.1L1L2

3.2

$d (x, z) \leq d (x, y) + d (y, z)$ : for every $k$ one has $∣ x_{k} - z_{k} ∣ \leq ∣ x_{k} - y_{k} ∣ + ∣ y_{k} - z_{k} ∣$ by [L3], so each partial sum of the left series is at most the corresponding partial sum of the sum of the two right series by [L2], and the inequality passes to the limits by [L2] and [L1]. This is (M3), so claim 2 holds.

step 2.1L1L2L3

3.3

Every $d$ -ball contains a basic product-open neighbourhood of its centre. Given $u \in Q$ and $ρ > 0$ , take $N$ with $2^{- N} < ρ / 2$ by step 1.2 and put $W : = {y \in Q : ∣ y_{k} - u_{k} ∣ < ρ / 2 for every k < N}$ , which is a basic product-open set containing $u$ by [A1] and [A2]. For $y \in W$ , splitting the series at $N$ gives $d (u, y) \leq (ρ / 2) \sum_{k < N} 2^{- (k + 1)} + \sum_{k \geq N} 2^{- (k + 1)} \leq ρ / 2 + 2^{- N} < ρ$ , by steps 1.1 and 2.1 with [L1] and [L2]. So $u \in W \subseteq B_{d} (u, ρ)$ .

step 1.1step 2.1step 1.2A1A2L1L2

4.1

$d (x, x) = 0$ , every term vanishing by [L3]. Conversely if $d (x, y) = 0$ then by step 3.1 every $∣ x_{j} - y_{j} ∣ 2^{- (j + 1)} \leq 0$ , so $∣ x_{j} - y_{j} ∣ = 0$ and $x_{j} = y_{j}$ for every $j$ by [L3] and [L4]; hence $x = y$ . This is (M1).

step 3.1L3L4

4.2

Every subbasic product-open set is $d$ -open. Let $O$ be open in $[0, 1]$ , let $x \in π_{j}^{- 1} [O]$ and take $ε > 0$ with ${t \in [0, 1] : ∣ t - x_{j} ∣ < ε} \subseteq O$ , available by [A2]. If $d (x, y) < ε 2^{- (j + 1)}$ then $∣ x_{j} - y_{j} ∣ 2^{- (j + 1)} < ε 2^{- (j + 1)}$ by step 3.1, so $∣ x_{j} - y_{j} ∣ < ε$ by [L4], so $y_{j} \in O$ ; hence $B_{d} (x, ε 2^{- (j + 1)}) \subseteq π_{j}^{- 1} [O]$ .

step 3.1A1A2L4L6

4.3

$T_{d}$ is contained in the product topology: by [L6] it suffices that every ball $B_{d} (x, r)$ be product-open, and for $z \in B_{d} (x, r)$ the triangle inequality of step 3.2 gives $B_{d} (z, r - d (x, z)) \subseteq B_{d} (x, r)$ with $r - d (x, z) > 0$ , while step 3.3 supplies a basic product-open $W$ with $z \in W \subseteq B_{d} (z, r - d (x, z))$ .

step 3.2step 3.3L6

5.1

The product topology is contained in $T_{d}$ : by step 4.2 every subbasic product-open set is $d$ -open, and $T_{d}$ is a topology containing them, hence contains the topology they generate, which is the product topology by [A1].

step 4.2A1L6

6.1

By steps 5.1 and 4.3 the metric topology of $d$ is the product topology on $Q$ , so $Q$ is metrizable; this is claim 3, and with steps 2.1 and 3.2 all three claims are proved.

step 2.1step 3.2step 5.1step 4.3∎

Remarks

The weights do two opposite jobs at once. Making the $k$ -th weight small ensures that the coordinates beyond a chosen index contribute at most $2^{- N}$ in total, which is what step 3.2 needs; keeping every weight strictly positive ensures that a single coordinate cannot be far apart without $d$ noticing, which is what step 4.2 needs. A weight sequence that failed either condition would fail to metrise the product topology.
Nothing here generalises for free. The argument uses that the index set is $N$ , through the convergent series of weights, and that each factor is bounded, through $∣ x_{k} - y_{k} ∣ \leq 1$ . Neither restriction is removable by this method, and no general theorem about metrizability of products is claimed on these pages (What the theory of these constructions still owes at this point in the reading order: preservation of quotient maps under products, separation beyond Hausdorff, and the invariants that tell the glued spaces apart).
The Hilbert cube is a product of subspaces, and that is unambiguous. Claim 1 of Products commute with subspaces; for infinite nonempty families, the closure identity $\overline{\prod A_{i}} = \prod \overline{A_{i}}$ uses the Axiom of Choice identifies the product of the subspaces $[0, 1] \subseteq R$ with the subspace $\prod_{k} [0, 1]$ of $R^{N}$ , so the metric above may equally be read as a metric on that subspace.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

102 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

Hilbert cube (Wikipedia) (standard reference, not scraped)
Product topology (Wikipedia) (standard reference, not scraped)
Metrizable space (Wikipedia) (standard reference, not scraped)

The Hilbert cube [0,1]N[0,1]N with the product topology is metrizable, by d(x,y)=∑k∣xk−yk∣/2 k+1d(x,y)=∑k​∣xk​−yk​∣/2k+1