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

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 tori are compact Hausdorff spaces separated by characters

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )) and let $T = R / Z$ be the torus with quotient map $q$ and quotient topology (The one-dimensional torus and its normalized Haar integral, The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection).

$T$ is compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) and Hausdorff (Hausdorff space: distinct points have disjoint open neighbourhoods; every metrizable space is Hausdorff and the indiscrete topology on two points is not), and the map $φ : T \to S^{1}, φ ([t]) : = (\cos 2 π t, \sin 2 π t),$ is a well-defined homeomorphism onto the Euclidean unit circle $S^{1} = {(x, y) \in R^{2} : x^{2} + y^{2} = 1}$ .
For every natural $n \geq 1$ the finite torus $T^{n}$ is compact and Hausdorff in the finite product topology (The one-dimensional torus and its normalized Haar integral), and the coordinate characters separate its points. Explicitly, define $χ_{j} (x) : = \exp (2 π i t)$ using any real representative $t$ with $q (t) = x_{j}$ ; this is well defined, and for distinct $x, y \in T^{n}$ some $j < n$ satisfies $χ_{j} (x) \neq χ_{j} (y)$ (The complex exponential by its power series).

Facts & Assumptions

[A1]

$q : R \to T$ is continuous and surjective, and a continuous image of a compact space is compact; $[0, 1]$ is compact (Heine-Borel by bisection: every closed bounded interval $[a, b]$ is compact, A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism, The one-dimensional torus and its normalized Haar integral).

[A2]

A continuous bijection from a compact space onto a Hausdorff space is a homeomorphism (A continuous image of a compact space is compact; a continuous real-valued map on a nonempty compact space attains a maximum and a minimum; and a continuous bijection from a compact space to a Hausdorff space is a homeomorphism).

[A3]

$t \mapsto (\cos t, \sin t)$ is a bijection of $[0, 2 π)$ onto $S^{1}$ ; sine and cosine have least positive common period $2 π$ , hence $\cos (x + 2 π m) = \cos x$ and $\sin (x + 2 π m) = \sin x$ for every integer $m$ , and $\exp (i θ) = \cos θ + i \sin θ$ ( $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle, The zero sets of sine and cosine and the least positive common period 2 pi, $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

[A4]

$\exp (2 π i u) = \exp (2 π i v)$ for reals $u, v$ if and only if $u - v \in Z$ , because both sides have the cartesian form of [A3] and the parametrisation of the circle is injective on $[0, 2 π)$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , $t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle).

[A5]

A finite product of compact spaces is compact, and arbitrary products preserve the Hausdorff property (A product of finitely many compact spaces is compact in the product topology, Arbitrary products preserve $T_{0}$ , $T_{1}$ , and Hausdorffness).

[A6]

The map induced on a quotient by a continuous map constant on the fibres is continuous (For a quotient map $q : X \to Y$ , a map out of $Y$ is continuous iff its composite with $q$ is; a continuous map on $X$ constant on the fibres of $q$ factors uniquely through $q$ ; and a composite of quotient maps is a quotient map).

[A7]

With $S : = ⋃_{k \in Z} (t - δ + k, t + δ + k)$ and $T : = ⋃_{k \in Z} (s - δ + k, s + δ + k)$ for $δ : = dist (s - t, Z) / 2 > 0$ when $s - t \notin Z$ , the two unions are disjoint saturated open sets, so their images are disjoint open neighbourhoods (The quotient topology of a surjection, quotient maps, saturated sets, and the quotient of a space by an equivalence relation with its canonical projection); and an integer part satisfies $n \leq r < n + 1$ (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ ).

Proof

technique · direct

Given: Countable Choice, the torus $T = R / Z$ with quotient map $q$ , and the map $φ$ .

1.1

$T$ is compact: $[0, 1]$ is compact, $q$ is continuous, and every class has a representative in $[0, 1]$ , so $T = q ([0, 1])$ is a continuous image of a compact space.

1.2

$T$ is Hausdorff: let $[s] \neq [t]$ , so that $s - t \notin Z$ and $δ : = dist (s - t, Z) / 2 > 0$ (positive because for $x : = s - t$ and an integer part $n$ of $x$ one has $∣ x - m ∣ \geq \min (x - n, n + 1 - x) > 0$ for every $m \in Z$ ). The saturated open sets of [A7] are the preimages of neighbourhoods of $[s]$ and $[t]$ and are disjoint, so the two classes have disjoint open neighbourhoods.

1.3

$φ$ is well defined and continuous: if $t^{'} - t \in Z$ then $t^{'} = t + m$ and $2 π t^{'} = 2 π t + 2 π m$ , so periodicity gives the same pair $(\cos, \sin)$ ; the map $t \mapsto (\cos 2 π t, \sin 2 π t)$ is continuous, being built from sine and cosine, which are differentiable and hence continuous, by composition with the continuous linear multiplication by $2 π$ , and it is constant on the fibres of $q$ , so it induces a continuous $φ$ by the universal property.

A3A6

1.4

The coordinate character $χ_{j} (x) : = \exp (2 π i t)$ , where $t \in R$ is any representative with $q (t) = x_{j}$ , is well defined by [A4]. If $x \neq y$ in $T^{n}$ , then $x_{j} \neq y_{j}$ for some $j < n$ . Were $χ_{j} (x) = χ_{j} (y)$ , [A4] would make the difference of chosen real representatives an integer and hence force $x_{j} = y_{j}$ , a contradiction. Thus the coordinate characters separate points.

2.1

$φ$ is bijective: it is surjective because every point of $S^{1}$ is $(\cos θ, \sin θ)$ for some $θ \in [0, 2 π)$ and then $θ / (2 π) \in [0, 1)$ represents a class mapping to it; and it is injective because if $φ ([s]) = φ ([t])$ , then choosing representatives $s^{'}, t^{'} \in [0, 1)$ of the two classes and using periodicity gives $(\cos 2 π s^{'}, \sin 2 π s^{'}) = (\cos 2 π t^{'}, \sin 2 π t^{'})$ with $2 π s^{'}, 2 π t^{'} \in [0, 2 π)$ , so $2 π s^{'} = 2 π t^{'}$ by injectivity of the parametrisation, whence $[s] = [t]$ .

step 1.3A3

2.2

For $n \geq 1$ the finite torus $T^{n}$ is a finite product of compact Hausdorff spaces, hence compact Hausdorff, by [A5], step 1.1 and step 1.2.

step 1.1step 1.2A5

3.1

By steps 1.1, 1.2 and 2.1, $φ$ is a continuous bijection from the compact space $T$ onto the Hausdorff Euclidean circle $S^{1}$ , hence a homeomorphism, which is claim 1.

step 1.1step 1.2step 2.1A2

4.1

Steps 3.1, 2.2 and 1.4 establish the homeomorphism $φ$ , compactness and Hausdorffness of every finite torus, and separation of points by the coordinate characters.

step 1.4step 2.2step 3.1∎

Depends on

Used by

Dependency tree · two levels

130 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

Theo Bühler and Dietmar Salamon, Functional Analysis — Example 2.66, pp.87–88 (standard reference, not scraped)
Gerald Teschl, Topics in Real and Functional Analysis, version November 17, 2017 — §2.5, pp.63–64 (standard reference, not scraped)