TheoremStatement: AI-adaptedProof: AI-generatedprecheck 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 $π_{i}$ is continuous, so $π_{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 · two levels

34 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

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)