TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31

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.

$Q^{n}$ is a countable dense subset of $R^{n}$ , and rational open boxes form a countable basis

Statement

Let $n \geq 1$ . The set $Q^{n}$ is countable and dense in $R^{n}$ . Moreover the rational open boxes

$\prod_{i < n} (a_{i}, b_{i}), a_{i}, b_{i} \in Q, a_{i} < b_{i},$

form a countable basis for the product topology on $R^{n}$ .

Facts & Assumptions

Given: $n \geq 1$ , the product $R^{n} = \prod_{i < n} R$ , and the rationals embedded in $R$ .

[L1]

$Q$ is countably infinite, and every finite power of an at most countable set is at most countable ( $Q$ is countably infinite, Every finite power of an at most countable set is at most countable).

[L2]

Every nonempty open subset of $R$ contains a rational point (Both $Q$ and $R ∖ Q$ are dense in $R$ , and every nonempty open subset of $R$ is uncountable).

[L3]

The product topology has a basis of finite-coordinate boxes, which for the finite index set $n$ are products of open subsets of $R$ (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).

[L4]

A family is a basis when each point of each open set lies in one of its members contained in that open set (Basis and subbasis for a topology, and the topology generated by a family of sets).

[L5]

Finite choices may be assembled into a tuple, and a subset of an at most countable set is at most countable (Every natural-number-indexed list of nonempty sets has a choice function on its family of values, Every subset of an at most countable set is at most countable).

[L6]

If $U \subseteq R$ is open and $x \in U$ , then some open interval about $x$ is contained in $U$ (Dictionary: for $A \subseteq R$ with the metric $d (x, y) = ∣ x - y ∣$ , continuity and uniform continuity of $f : A \to R$ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of $R$ is compact in the open-cover sense of $R$ exactly when it is a compact metric subspace).

Proof

technique · constructive

1.1

By [L1], $Q^{n}$ is at most countable. It is infinite because the injection $q \mapsto (q, 0, \dots, 0)$ embeds $Q$ in it, hence it is countable.

1.2

Let $U = \prod_{i < n} U_{i}$ be a nonempty basic product-open set. Every $U_{i}$ is nonempty and open, so [L2] gives a rational $q_{i} \in U_{i}$ ; finite choice supplies the tuple $q = (q_{i})_{i < n} \in Q^{n} \cap U$ .

L2L5choose

1.3

Let $x \in U = \prod_{i < n} U_{i}$ be a basic product-open neighbourhood. For each $i < n$ , use [L6] to choose $r_{i} > 0$ with $(x_{i} - r_{i}, x_{i} + r_{i}) \subseteq U_{i}$ , then use [L2] to choose rationals $x_{i} - r_{i} < a_{i} < x_{i} < b_{i} < x_{i} + r_{i} .$ Finite choice assembles these choices, and then $x \in \prod_{i < n} (a_{i}, b_{i}) \subseteq U$ .

L2L5L6choose

2.1

Every nonempty open subset contains a nonempty basic product-open set about each of its points by [L3], so step 1.2 shows that every nonempty open subset meets $Q^{n}$ . Thus $Q^{n}$ is dense.

L3step 1.2

3.1

Step 1.3 and [L4] show that rational open boxes form a basis. They are indexed by a subset of $Q^{2 n}$ , which is at most countable by [L1], so the basis is at most countable by [L5].

L1L4L5step 1.3∎

Depends on

Used by

Dependency tree · two levels

72 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

Euclidean space (standard reference, not scraped)
Separable space (Wikipedia) (standard reference, not scraped)

QnQn is a countable dense subset of RnRn, and rational open boxes form a countable basis