LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-10

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.

Continuous injections of sequence spaces into the real line

Statement

In ZF the map

$j : 2^{N} \to R, j (b) = \sum_{k = 0}^{\infty} 2 b (k) 3^{- k - 1}$

is a continuous injection. If $h : N^{N} \to 2^{N}$ is the block-coding map, then $e = j \circ h$ is a continuous injection of Baire space into $R$ .

Facts & Assumptions

[F1]

The Cantor set is exactly the set of $\sum_{k \geq 1} a_{k} 3^{- k}$ with every $a_{k} \in {0, 2}$ , and this gives a bijection with ${0, 1}^{N}$ supplies convergence and injectivity for these zero-based ternary series.

[F2]

Cantor and Baire sequence spaces and coordinate codings supplies the continuous injective block coding and the cylinder topologies.

[F3]

Continuity of a map of topological spaces at a point and globally gives the open-neighbourhood criterion for continuity.

Proof

Given: The two explicit series and block maps, with no choice assumption.

1.1

Each digit $2 b (k)$ is zero or two, so F1 applies to give a convergent series and injectivity of j. If b,c agree in their first n coordinates, subtraction of their convergent series and the geometric tail bound give

F1F2

$∣ j (b) - j (c) ∣ \leq \sum_{k = n}^{\infty} 2 3^{- k - 1} = 3^{- n} .$

The equality follows from the finite geometric sum and its limit. Since $3^{n} \geq n + 1$ , these tails tend to zero. Given an open neighbourhood O of j(b), take a radius $ϵ > 0$ ball contained in it and n with $3^{- n} < ϵ$ . The cylinder $N_{b ↾ n}$ then maps into O by the inequality. Thus j is continuous by F3 and F2. [F1, F2, F3]

2.1

By F2 h is injective and continuous. If $e (x) = e (y)$ , injectivity of j gives $h (x) = h (y)$ and injectivity of h gives x=y. For a real open O, $e^{- 1} [O] = h^{- 1} [j^{- 1} [O]]$ is open by continuity of both maps, proving continuity of e. In particular j sends the zero sequence to zero and the all-one sequence to one, as the same geometric sum shows. QED.

F2F3step 1.1

Depends on

Used by

Every set of reals is Borel False statement

Dependency tree · two levels

31 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

Definition 1.7 and Exercise 1.11, pp4–5, sequence-space coding context; ternary-series calculation is the explicit local argument from thm-cantor-set-ternary-description, not a claimed Marker theorem (standard reference, not scraped)