ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-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.

The isolated-point repair recovers a choice function

Example

Take the three nonempty sets $A_{0} = {0, 1}$ , $A_{1} = N$ and $A_{2} = R$ , and form the repaired coordinates $X_{A_{j}}$ of The isolated-point repair of Kelley's choice space. Assume the compact- $T_{1}$ product hypothesis: every product of compact $T_{1}$ spaces is compact. In the product $X : = X_{A_{0}} \times X_{A_{1}} \times X_{A_{2}}$ the closed constraints $C_{j} : = {x : x_{j} \in A_{j}}$ have the finite intersection property, so compactness of $X$ produces a point whose three coordinates are a choice tuple.

Facts & Assumptions

Given: The three sets, their repaired coordinates $X_{A_{j}} = A_{j} ⊔ {\infty_{j}}$ , and the hypothesis that every product of compact $T_{1}$ spaces is compact.

[F1]

Each $X_{A_{j}}$ is compact $T_{1}$ and $A_{j}$ is a closed subspace of it (The isolated-point repair of Kelley's choice space, $T_{0}$ (Kolmogorov) and $T_{1}$ (Frechet) spaces).

[F2]

In a product, the cylinder $π_{j}^{- 1} [A_{j}]$ is closed when $A_{j}$ is closed in the factor, and a space is compact exactly when every family of closed sets with the finite intersection property has nonempty intersection (The product set $\prod_{i \in I} X_{i}$ of functions choosing a point in each factor, the projections, the box topology, and the product topology as the initial topology of the projections; the empty product is a one-point space, A space is compact exactly when every family of closed subsets with the finite intersection property has nonempty intersection, Finite intersection property).

[F3]

The hypothesis that every product of compact $T_{1}$ spaces is compact makes $X$ compact (The compact T1 product theorem is equivalent to AC, Open cover, subcover, and compact topological space; a compact subset is a subspace that is compact in its own right).

[L1]

Let $A = {A_{0}, A_{1}, A_{2}}$ . If a product point $x$ satisfies $x_{j} \in A_{j}$ for every $j \in {0, 1, 2}$ , then for each $S \in A$ let $j (S)$ be the least $j \in {0, 1, 2}$ with $S = A_{j}$ and define $g (S) = x_{j (S)}$ . The least index exists because $S$ occurs in the displayed finite list, and $g (S) = x_{j (S)} \in A_{j (S)} = S$ . Hence $g$ has domain $A$ and is a choice function on $A$ (Choice function, Every natural-number-indexed list of nonempty sets has a choice function on its family of values).

Verification

1.1

The three cylinders $C_{0}, C_{1}, C_{2}$ are closed in $X$ by [F1] and [F2].

givenF1F2

1.2

Each single cylinder is nonempty: the point with one coordinate $0$ (or any other element of $A_{j}$ ) and the artificial values $\infty$ at the other two coordinates lies in it; the artificial values are available because $\infty_{k} \in X_{A_{k}}$ for every $k$ .

givenF1

2.1

For the pair ${j, k}$ the point with prescribed values in $A_{j}$ and $A_{k}$ and $\infty$ in the remaining coordinate lies in $C_{j} \cap C_{k}$ , so the family has the finite intersection property; for the triple the point $(0, 0, 0)$ lies in $C_{0} \cap C_{1} \cap C_{2}$ .

step 1.2F2

3.1

By [F3] the product $X$ is compact, so by [F2] the intersection $C_{0} \cap C_{1} \cap C_{2}$ is nonempty. Choose $x$ in this intersection. Then $x_{j} \in A_{j}$ for all three indices, and the function $g$ defined in [L1] has domain $A = {A_{0}, A_{1}, A_{2}}$ and satisfies $g (S) \in S$ for every $S \in A$ . Thus $g$ is the required choice function.

step 2.1F2F3L1

4.1

For a finite list of $n$ sets, the same least-index construction converts a point in the $n$ closed cylinders into a choice function on the underlying set-family. In the general AC argument the factors are instead indexed by the family $A$ itself, so a product point $x$ with $x_{A} \in A$ directly defines the choice function $A \mapsto x_{A}$ ; compactness supplies such a point after finite choice verifies the cylinders' finite-intersection property. [step 3.1, F2, L1, Every natural-number-indexed list of nonempty sets has a choice function on its family of values] ∎

Depends on

Used by

Nothing in the library uses this result yet.

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)