TheoremStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passverified 2026-08-05 (claude-sonnet-5)

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.

Assuming the ultrafilter lemma, an arbitrary product of compact Hausdorff spaces is compact

Statement

Assume the ultrafilter lemma. If $(X_i)_{i\in I}$ is any family of compact Hausdorff spaces, then $\prod_{i\in I}X_i$ , with its product topology, is compact.

Facts & Assumptions

Given: Compact Hausdorff spaces $X_i$ , their product $P$ , and a universal net $x_d$ in $P$ .

[L1]

A continuous image of a universal net is universal (The image of a universal net under any map is universal, and a continuous map preserves its limits).

[L2]

Assuming the ultrafilter lemma, a space is compact if and only if every universal net in it converges (Assuming the ultrafilter lemma, a space is compact if and only if every universal net converges).

[L3]

In a Hausdorff space a net has at most one limit (A topological space is Hausdorff if and only if every net has at most one limit).

[L4]

Basic product neighbourhoods restrict only finitely many coordinates (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).

Proof

technique · constructive

1.1

For every $i\in I$ , the projection $\pi_i$ is continuous, so $\pi_i(x_d)$ is universal by [L1] and converges in compact $X_i$ by [L2]. Its limit $p_i$ is unique by [L3].

L1L2L3

2.1

The uniqueness in step 1.1 defines a point $p\in\prod_{i\in I}X_i$ , namely the function $i\mapsto p_i$ , rather than choosing a family of limits.

step 1.1L3construct

2.2

Let $N$ be a neighbourhood of $p$ in $P$ . By [L4], it contains a basic product neighbourhood restricting a finite set $J\subseteq I$ ; for each $i\in J$ , the coordinate net is eventually in its prescribed neighbourhood of $p_i$ . Directedness supplies one index after the finitely many thresholds, and after it $x_d\in N$ . Thus $x_d\to p$ .

step 1.1L4

3.1

Every universal net in $P$ converges by step 2.2. The converse direction of [L2] therefore makes $P$ compact.

step 2.2L2discharge-construct∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 93 results over 13 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

WVU Math 581 Topology I (standard reference, not scraped)
Tychonoff's theorem (Wikipedia) (standard reference, not scraped)
Boolean prime ideal theorem (Wikipedia) (standard reference, not scraped)
Net (mathematics) (Wikipedia) (standard reference, not scraped)