Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26
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 complement of a compact plane set has exactly one unbounded connected component

Statement

Let K⊆C be compact. Then C∖K has exactly one unbounded connected component U∞, and every other component is bounded. Moreover, whenever R>0 satisfies K⊆{z:∣z∣≤R}, the exterior {z:∣z∣>R} is contained in U∞.

The empty set is covered: C∖∅=C has the single component C, which is unbounded.

Facts & Assumptions

Given: A compact set K⊆C; the plane is read as R2 with its Euclidean metric through C=R[x]/(x2+1) as the Euclidean plane and as a normed real algebra: what the identification preserves.

[L1]

For c∈C and R>0, the set {z:∣z−c∣>R} is path-connected and a connected subset of C (The exterior of a closed disc in the plane is path-connected).

[L2]

The connected component C(x) is the union of all connected subsets containing x (Connected components, quasicomponents, and totally disconnected spaces).

[L3]

C(x) contains every connected subset containing x; distinct components are disjoint; every point lies in its own component, and the components cover the space (The components of a space are its maximal connected subsets, they partition it, and each of them is closed).

[L5]

A compact subset of a metric space is closed and bounded (A compact subset of a metric space is closed and bounded).

[L6]

A subset A of a metric space is bounded when A=∅ or A⊆B(x0,r) for some x0 and some real r>0 (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space, Open ball, closed ball and sphere in a metric space).

[L8]

For n≥1, Rn is polygonally connected and connected (Rn is polygonally connected, connected, locally path-connected and locally connected).

[L9]

For every real ε>0 there is a natural n≥1 with 1/n<ε (For every ε>0 in a complete ordered field there is a natural n≥1 with 1/n<ε).

Proof

technique · direct
1.1givenL5L6L7

By [L5] the set K is closed and bounded, so by [L6] there are x0 and s>0 with K⊆B(x0,s), and then K⊆{z:∣z∣≤R} for R=∣x0∣+s>0; if K=∅ any R>0 serves. By [L7] the complement C∖K is open.

1.2givenL1L6L9

Fix any R>0 with K⊆{z:∣z∣≤R} and put ER={z:∣z∣>R}. Then ER⊆C∖K, and ER is a connected subset of C by [L1]; it is nonempty, since 2R∈ER, and unbounded, since for every real r>0 and every x0 the number R+∣x0∣+r has modulus exceeding R and lies outside B(x0,r), so no ball of [L6] contains ER.

2.1step 1.1step 1.2L2L3L6

Let z0∈ER and let U∞:=C(z0) be its component in C∖K. The set ER is a connected subset of C∖K containing z0, so ER⊆U∞ by [L2] and [L3]; hence U∞ is unbounded by step 1.2 and [L6]. This holds for every admissible R, which is the final clause of the statement.

3.1step 2.1L3L6

Let C be a component of C∖K with C≠U∞. By [L3] the two are disjoint, so C∩ER=∅ by step 2.1, that is C⊆{z:∣z∣≤R}⊆B(0,R+1); hence C is bounded by [L6].

4.1step 2.1step 3.1L3L4L8∎

Steps 2.1 and 3.1 give exactly one unbounded component, namely U∞, with every other component bounded. When K=∅ the complement is C, which is connected by [L8], so by [L3] and [L4] it is its own single component and that component is U∞.

Depends on

Used by

Dependency tree · two levels

55 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