Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck 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.

Rn\mathbb{R}^n as the product of nn copies of the real line: the product topology is the Euclidean topology and the projections are continuous, open and surjective

Example

Fix nNn \in \mathbb{N} with n1n \ge 1 and give R\mathbb{R} its usual topology (The absolute value makes R\mathbb{R} a metric space: d(x,y)=xyd(x,y) = |x-y| is a metric, its open balls are the intervals (xr,x+r)(x-r, x+r), and it is unbounded, Metrizable space: a topological space whose topology is induced by some metric; metrizability is topological, the metric is not). Let Rn=k<nR\mathbb{R}^n = \prod_{k<n} \mathbb{R} carry the product topology (The product set iIXi\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), with projections πj(x)=xj\pi_j(x) = x_j. Then:

  1. The product topology is the Euclidean topology. It is the metric topology of dd_\infty, and equally of d1d_1 and of d2d_2 (Rn\mathbb{R}^n as the set of functions nRn \to \mathbb{R}, and d1d_1, d2d_2, dd_\infty are metrics on it, For n1n \ge 1 the product topology on nn copies of the usual topology of R\mathbb{R} is the metric topology of dd_\infty on Rn\mathbb{R}^n, and hence also of d1d_1 and d2d_2, so Rn\mathbb{R}^n as a product and Rn\mathbb{R}^n as a metric space are one space); in particular Rn\mathbb{R}^n with the product topology is metrizable, and "open in Rn\mathbb{R}^n" has one meaning.
  2. A basis of open boxes. The sets k<n(ak,bk)\prod_{k<n}(a_k, b_k) with ak<bka_k < b_k for every k<nk < n form a basis (Intervals of R\mathbb{R}: the nine order-convex forms, nondegeneracy, and length), since the dd_\infty-ball B(x,r)B(x,r) is exactly the box k<n(xkr, xk+r)\prod_{k<n}(x_k - r,\ x_k + r).
  3. The projections are continuous, open and surjective. Continuity and openness are the general facts (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, claims 1 and 3; Continuity of a map of topological spaces at a point and globally, Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological). Surjectivity needs no choice principle here: for tRt \in \mathbb{R} the constant function xx with xk=tx_k = t for every k<nk<n satisfies πj(x)=t\pi_j(x) = t.
  4. Componentwise continuity. For a space ZZ, a function h:ZRnh : Z \to \mathbb{R}^n is continuous if and only if each of its nn components hk=πkh:ZRh_k = \pi_k \circ h : Z \to \mathbb{R} is (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). This is the statement usually quoted as "a vector-valued map is continuous exactly when its coordinate functions are", and here it is a special case of a theorem about arbitrary products.

Facts & Assumptions

Given: A natural n1n \ge 1; Rn=k<nR\mathbb{R}^n = \prod_{k<n}\mathbb{R} with the product topology; the projections πj\pi_j; a topological space ZZ and a function h:ZRnh : Z \to \mathbb{R}^n; a real tt and an index j<nj < n.

[A1]

Rn\mathbb{R}^n is the set of functions nRn \to \mathbb{R} and d(x,y)=max{xkyk:k<n}d_\infty(x,y) = \max\{|x_k-y_k| : k<n\} is a metric on it for n1n \ge 1 (Rn\mathbb{R}^n as the set of functions nRn \to \mathbb{R}, and d1d_1, d2d_2, dd_\infty are metrics on it).

Verification

technique · direct
1.1

Claim 1 is [L1] verbatim, together with the observation that a topology induced by a metric makes the space metrizable.

A1L1
1.2

The constant function xx with xk:=tx_k := t for every k<nk < n is an element of Rn\mathbb{R}^n, since it is a function nRn \to \mathbb{R}, and πj(x)=xj=t\pi_j(x) = x_j = t.

A1
1.3

Claims 3 and 4, apart from surjectivity, are [L2] read for the family of nn projections.

L2
2.1

Every dd_\infty-ball is a box of bounded open intervals of equal length, by [L1], and the balls form a basis of the metric topology by [L3]; so the boxes k<n(ak,bk)\prod_{k<n}(a_k,b_k) with ak<bka_k < b_k include a basis and are themselves open by [L4], hence form a basis. This is claim 2.

step 1.1L1L3L4
2.2

By step 1.2 the projection πj\pi_j is surjective, with no appeal to a choice principle, the point xx being written down. This completes claim 3 with step 1.3.

step 1.2step 1.3
3.1

Steps 1.1, 2.1, 2.2 and 1.3 establish claims 1, 2, 3 and 4 respectively.

step 1.1step 1.3step 2.1step 2.2

Remarks

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 121 results over 21 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