LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6-luna)

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.

Finite-dimensional Euclidean space with its Borel sigma-algebra is standard Borel

Statement

For every natural $n \geq 1$ , let $R^{n}$ be the set of functions $x : n \to R$ with its finite-product topology and Borel sigma-algebra (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, The Borel sigma-algebra of a topological space). Then $(R^{n}, B (R^{n}))$ is standard Borel.

Facts & Assumptions

Given: A natural $n \geq 1$ ; $R^{n}$ with its finite-product topology; the Euclidean metric $d_{2}$ and maximum metric $d_{\infty}$ from $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it.

[F1]

The functions $x : n \to R$ form $R^{n}$ ; $d_{\infty}$ is a metric, and its balls are defined by the metric topology ( $R^{n}$ as the set of functions $n \to R$ , and $d_{1}$ , $d_{2}$ , $d_{\infty}$ are metrics on it, 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).

[F2]

Every nonempty finite set of real numbers has a maximum and minimum, each belonging to the set and bounding it on the corresponding side (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set).

[F3]

For $u \in R$ , $u^{2} = ∣ u ∣^{2}$ ; finite sums of nonnegative terms are nonnegative, each term is at most the sum, sums are monotone, and $\sum_{i < n} c = n c$ (Basic properties of the absolute value, Laws of finite sums and finite products).

[F4]

Nonnegative numbers have unique nonnegative square roots; square-root order is monotone, and the real image of a natural $n \geq 1$ is positive (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squaring is monotone on the nonnegatives, Canonical naturals are positive and strictly increasing).

[F5]

The Euclidean metric $d_{2}$ on $R^{n}$ is complete for $n \geq 1$ ( $R$ and $R^{n}$ for $n \geq 1$ with the Euclidean metric are complete, componentwise from the Cauchy criterion in $R$ ).

[F6]

$Q^{n}$ is at most countable and dense, and rational open boxes form a basis for the finite-product topology on $R^{n}$ ( $Q^{n}$ is a countable dense subset of $R^{n}$ , and rational open boxes form a countable basis).

[F7]

Polish means separable and admitting a compatible complete metric; separable means having an at most countable dense subset (Polish spaces are separable completely metrizable spaces, Separability: the existence of an at most countable dense subset).

[F8]

Standard Borel means measurably isomorphic to the Borel space of a Polish topology; a Borel sigma-algebra is generated by the open sets (Standard Borel spaces, The Borel sigma-algebra of a topological space).

[F9]

A metric Cauchy sequence has tails whose pairwise distances are below each positive rational tolerance, and metric convergence means distance to the limit tends to zero (Cauchy sequence in a metric space, Convergence of a sequence in a metric space: $x_{k} \to x$ iff $d (x_{k}, x) \to 0$ in $R$ ).

[F10]

Every nonempty real interval contains a rational number, so each positive real tolerance has a smaller positive rational tolerance (The rationals embed densely in the reals).

Proof

Proof technique: compare the maximum metric topology with the product topology, then use completeness and rational density.

1.1F1F2F6

Every $d_{\infty}$ -ball about $x$ of radius $r > 0$ is the product box $\prod_{i < n} (x_{i} - r, x_{i} + r)$ , so it is open in the product topology. Conversely, let $U$ be product-open and $x \in U$ . By [F6], choose a rational box $Q = \prod_{i < n} (a_{i}, b_{i})$ with $x \in Q \subseteq U$ . The finite set $S = {x_{i} - a_{i}, b_{i} - x_{i} : i < n}$ is nonempty because $n \geq 1$ , and every member is positive. By [F2], $r = \min S$ exists and is positive. If $d_{\infty} (x, y) < r$ , then $∣ x_{i} - y_{i} ∣ \leq d_{\infty} (x, y) < r \leq x_{i} - a_{i}$ and $∣ x_{i} - y_{i} ∣ < r \leq b_{i} - x_{i}$ for every $i < n$ , hence $y \in Q \subseteq U$ . Thus each product-open set is $d_{\infty}$ -open, and the topologies agree.

1.2F1F2F3F4algebra

Fix $x, y \in R^{n}$ , put $u_{i} = x_{i} - y_{i}$ and $M = d_{\infty} (x, y)$ . By [F1] and [F2], $M = ∣ u_{j} ∣$ for some $j < n$ and $0 \leq ∣ u_{i} ∣ \leq M$ for every $i < n$ . Hence [F3] gives $M^{2} = u_{j}^{2} \leq \sum_{i < n} u_{i}^{2} = d_{2} (x, y)^{2}$ , so [F4] yields $M \leq d_{2} (x, y)$ . Also $u_{i}^{2} = ∣ u_{i} ∣^{2} \leq M^{2}$ for each $i$ , whence $d_{2} (x, y)^{2} = \sum_{i < n} u_{i}^{2} \leq \sum_{i < n} M^{2} = n M^{2}$ by [F3]. Since $n > 0$ , [F4] makes $\sqrt{n} M$ nonnegative and $(\sqrt{n} M)^{2} = n M^{2}$ ; square-root monotonicity now gives $d_{2} (x, y) \leq \sqrt{n} M$ . Thus $d_{\infty} \leq d_{2} \leq \sqrt{n} d_{\infty}$ for all pairs.

2.1F9F10step 1.2algebra

Let $(x^{(m)})$ be $d_{\infty}$ -Cauchy and fix a positive rational $ε$ . By [F10], choose a positive rational $ρ < ε / (1 + \sqrt{n})$ . The Cauchy condition [F9] gives a tail on which $d_{\infty} (x^{(m)}, x^{(l)}) < ρ$ . Step 1.2 then gives $d_{2} (x^{(m)}, x^{(l)}) \leq \sqrt{n} d_{\infty} (x^{(m)}, x^{(l)}) < \sqrt{n} ρ < ε$ , so the sequence is $d_{2}$ -Cauchy.

3.1F5F9step 1.2step 2.1

By [F5], this sequence has a $d_{2}$ -limit $x \in R^{n}$ . Step 1.2 gives $d_{\infty} (x^{(m)}, x) \leq d_{2} (x^{(m)}, x) \to 0$ ; by [F9] this is convergence in $d_{\infty}$ . Therefore $d_{\infty}$ is complete.

4.1F6F7step 1.1step 3.1

By [F6], $Q^{n}$ is at most countable and dense in the product topology. Step 1.1 identifies that topology with the $d_{\infty}$ topology, so the same subset is dense for $d_{\infty}$ . Thus the product topology is separable by [F7], and step 3.1 supplies its compatible complete metric. Consequently $R^{n}$ with the product topology is Polish.

5.1F8step 1.1step 4.1∎

The identity from $(R^{n}, B (R^{n}))$ to the Polish space of step 4.1 is a bijection. The topologies are identical by step 1.1, so they have the same open sets and therefore, by [F8], the same Borel sigma-algebra. The identity is thus a measurable isomorphism as required by the definition of standard Borel.

Depends on

Used by

Dependency tree · two levels

83 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

O. Biskup, MATH 275D notes, Chapter 2: Kolmogorov Extension Theorem (standard reference, not scraped)