PropositionStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24

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.

The Hawaiian earring is compact and path-connected

Statement

For every integer $n \geq 1$ , let $C_{n}$ be the circle of radius $1 / n$ centred at $(1 / n, 0)$ , and put

$H = ⋃_{n \geq 1} C_{n} \subseteq R^{2} .$

The Hawaiian earring $H$ is compact and path-connected.

Facts & Assumptions

Given: The circles $C_{n} = S_{2} ((1 / n, 0), 1 / n)$ for integers $n \geq 1$ , and their union $H$ .

[F1]

A Euclidean sphere $S_{2} (c, r)$ is the set of points $x$ with $∥ x - c ∥_{2} = r$ (Euclidean spheres and closed balls as subspaces of $R^{n}$ ).

[L1]

A subset of $R^{2}$ is compact exactly when it is closed and bounded (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line).

[F2]

A space is path-connected when every pair of its points can be joined by a continuous path in it (Paths, path-connected spaces and path components).

[L2]

The circle $R / Z$ is path-connected, and its standard map to the geometric unit circle is a homeomorphism ( $R / Z$ is compact and path-connected, $[t] \mapsto (\cos 2 π t, \sin 2 π t)$ is a homeomorphism from $R / Z$ to the unit circle).

[L3]

A map into $R^{m}$ is continuous exactly when its component functions are continuous; sums and scalar multiples of continuous Euclidean-valued maps are continuous (A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions).

[L4]

The Euclidean norm satisfies the reverse triangle inequality $∣ ∥ u ∥_{2} - ∥ v ∥_{2} ∣ \leq ∥ u - v ∥_{2}$ and is continuous (The finite and reverse triangle inequalities for a norm; and for $n \geq 1$ every norm $N$ on $R^{n}$ satisfies $N (x) \leq C ∥ x ∥_{1}$ and is Lipschitz, hence continuous, for $d_{2}$ ).

[L5]

For every real $ε > 0$ there is an integer $N \geq 1$ with $1 / N < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Proof

technique · direct

1.1

Each $C_{n}$ contains the origin because its centre has norm $1 / n$ , and its radius is positive because $n \geq 1$ . Thus the displayed union is nonempty and no circle of radius $1 / 0$ occurs.

givenF1constructalgebra

2.1

If $x \in C_{n}$ , then $∥ x ∥_{2} \leq ∥ x - (1 / n, 0) ∥_{2} + 1 / n = 2 / n \leq 2$ , so $H$ is bounded.

step 1.1F1algebra

2.2

Each $C_{n}$ is closed: if $x \notin C_{n}$ , then $η = ∣ ∥ x - (1 / n, 0) ∥_{2} - 1 / n ∣ / 2 > 0$ , and [L4] shows that the ball of radius $η$ about $x$ misses $C_{n}$ . Now let $x \notin H$ and write $d = ∥ x ∥_{2} > 0$ . By [L5], choose $N \geq 1$ with $2 / N < d / 2$ . Every $C_{n}$ with $n \geq N$ lies in the ball of radius $d / 2$ about $0$ , while the union of the circles with $1 \leq n < N$ is a finite, possibly empty, closed union that misses $x$ . Intersecting a neighbourhood of $x$ disjoint from that finite union with the ball of radius $d / 2$ about $x$ gives a neighbourhood disjoint from all of $H$ . Hence $H$ is closed.

step 1.1F1L4L5algebra

3.1

Steps 2.1 and 2.2 make $H$ closed and bounded in $R^{2}$ , so it is compact by [L1].

step 2.1step 2.2L1

4.1

The affine map $z \mapsto (1 / n, 0) + (1 / n) z$ carries the unit circle homeomorphically onto $C_{n}$ , so [L2] and [L3] make each $C_{n}$ path-connected. Given $x \in C_{m}$ and $y \in C_{n}$ , join $x$ to the common origin inside $C_{m}$ and then the origin to $y$ inside $C_{n}$ ; concatenating the paths gives a path in $H$ . Thus $H$ is path-connected.

step 1.1F2L2L3construct∎

Depends on

Used by

The Hawaiian earring retracts onto each of its circles Example
FALSE: every compact path-connected subset of ℝ² has a universal cover False statement

Dependency tree · two levels

80 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

Allen Hatcher, Algebraic Topology, Example 1.25 (standard reference, not scraped)