LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

The isolated-point repair of Kelley's choice space

Statement

Let $A$ be a set and let $A_{c}$ be $A$ with the cofinite topology (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies). Then the topological sum $X_{A} : = A_{c} ⊔ {\infty}$ of $A_{c}$ with a one-point space (The disjoint union (coproduct) $⨆_{i} X_{i}$ with the final topology of the canonical injections: a set is open exactly when each of its traces is) is compact (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right) and $T_{1}$ ( $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces), and $A$ is a closed subspace of $X_{A}$ (Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace). This is the repaired coordinate of the product-compactness argument. We identify each summand with its tagged copy in the disjoint union, so the added point is distinct from every point of $A$ . This is in contrast with the cofinite topology on $A \cup {\infty}$ itself.

Facts & Assumptions

Given: A set $A$ ; the cofinite space $A_{c}$ ; the sum $X_{A} = A_{c} ⊔ {\infty}$ .

[F1]

In the cofinite topology the open sets are $\emptyset$ and the sets with finite complement, and the closed sets are the whole space and the finite sets; the cofinite space is $T_{1}$ (The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[F2]

In the topological sum a subset $U \subseteq X_{A}$ is open exactly when its trace $U \cap A$ is open in $A_{c}$ ; independently, its trace on the singleton summand may be either $\emptyset$ or ${\infty}$ , both of which are open. Thus $\emptyset$ and ${\infty}$ are open, and the summand $A$ is clopen (The disjoint union (coproduct) $⨆_{i} X_{i}$ with the final topology of the canonical injections: a set is open exactly when each of its traces is, A map out of a disjoint union is continuous iff each of its restrictions is; the canonical injections are open and closed embeddings; and each summand is clopen in the union).

[F3]

A space is compact when every open cover has a finite subcover; in particular, the empty space and a one-point space are compact directly from this definition (Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[F4]

For a function $F$ with domain a natural number $n$ , if each $F (j)$ is nonempty then its family of values $F [n]$ has a choice function (Every natural-number-indexed list of nonempty sets has a choice function on its family of values). A finite set admits a bijection from some natural number; fixing one such enumeration for one finite set is a single existential instantiation (Finite, countably infinite, countable, uncountable).

Proof

technique · direct

1.1

Assume $X_{A}$ is nonempty, which it is because $\infty$ is one of its points.

given

2.1

The cofinite space $A_{c}$ is compact. Given an open cover $U$ , if $A = \emptyset$ the empty subfamily covers it. Otherwise fix $a \in A$ and $U_{0} \in U$ containing $a$ . By [F1] the complement $C = A ∖ U_{0}$ is finite. Fix a natural number $n$ and a bijection $e : n \to C$ by [F4], including the empty enumeration when $C = \emptyset$ . Define $F (j) = {U \in U : e (j) \in U}$ for $j < n$ . Every value is nonempty because $U$ covers $A$ . Apply [F4] to this function and let $c$ choose from its family of values. Then $U_{0}$ together with the list $c (F (j))$ , $j < n$ , is a finite subcover. No simultaneous choice of enumerations for an infinite family is involved.

step 1.1F1F3F4

2.2

$X_{A}$ is $T_{1}$ : for distinct points $x, y$ of $X_{A}$ , the set $X_{A} ∖ {y}$ is open — if $y = \infty$ it is $A$ , which is cofinite in $A$ and open in the sum by [F2]; if $y \in A$ it is $(A ∖ {y}) \cup {\infty}$ , whose trace on $A$ is cofinite, hence open in the sum by [F2] — and symmetrically for $X_{A} ∖ {x}$ .

step 1.1F1F2

3.1

Let $V$ be an open cover of $X_{A}$ . By [F2], ${V \cap A : V \in V}$ is an open cover of $A_{c}$ . Step 2.1 and [F3] give either the empty subcover or a finite list of traces $W_{j}$ , $j < m$ , covering $A$ . Define $G (j) = {V \in V : V \cap A = W_{j}}$ for $j < m$ . Each value is nonempty by the definition of the trace family. Apply [F4] to $G$ and choose $d$ on its family of values; the list $d (G (j))$ , $j < m$ , covers $A$ . Fix one $V_{\infty} \in V$ containing $\infty$ , which exists since $V$ covers $X_{A}$ . Adjoining it to this finite list covers $X_{A}$ , proving compactness. When $A$ is empty take $m = 0$ , so $V_{\infty}$ alone suffices.

step 2.1F2F3F4

4.1

$A$ is closed in $X_{A}$ : its complement ${\infty}$ is open in the sum by [F2], and the subspace topology that $A$ inherits is the cofinite topology of $A_{c}$ ; hence $A$ is a closed subspace of $X_{A}$ in the sense of Subspace topology: the traces of the open sets, its closed sets and its bases, the continuity of the inclusion, and the characteristic property of a map into a subspace.

step 2.2F1F2∎

Remarks

Why the naive coordinate fails. If instead $A \cup {\infty}$ carries the cofinite topology, then for infinite $A$ the set $A$ is not closed: its complement ${\infty}$ is finite and hence closed, while a proper closed set in a cofinite space must itself be finite. Thus $A$ is open but not closed. That failure is the content of the companion counterexample.
What compactness costs. Compactness of $A_{c}$ uses finite choice only, and the sum with a point adds no further cost, so the repaired coordinate is available in ZF; this is what makes it usable in the product argument below.

Depends on

Used by

Kelley's cofinite set is not closed Counterexample
The isolated-point repair recovers a choice function Example
The compact T1 product theorem is equivalent to AC Theorem

Dependency tree · two levels

33 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

Kyriakos Keremedis and Eleftherios Tachtsis, Wallman Compactifications and Tychonoff's Compactness Theorem in ZF (standard reference, not scraped)
J. L. Kelley, The Tychonoff product theorem implies the axiom of choice, Fund. Math. 37 (1950), 75-76 (standard reference, not scraped)