Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (z-ai/glm-5.2)audited 2026-07-31
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 countable choice, every countably compact paracompact Hausdorff space is compact

Statement

Assume the Axiom of Countable Choice. Every countably compact paracompact Hausdorff space is compact.

Facts & Assumptions

Given: Countable choice and a countably compact paracompact Hausdorff space XX.

[A1]

Countable choice supplies a choice function for every sequence of nonempty sets (The Axiom of Countable Choice (ACω\mathrm{AC}_\omega)).

[F1]

Countable compactness tests at most countable open covers, while compactness tests all open covers (Countably compact, Lindel"of, sequentially compact, limit point compact and σ\sigma-compact spaces, and relatively compact subsets).

[L2]

Under countable choice, a countable union of at most countable sets is at most countable (Countable unions of at most countable sets, assuming ACω\mathrm{AC}_\omega, Finite, countably infinite, countable, uncountable).

Proof

technique · direct
1.1

Let U\mathcal U be an arbitrary open cover, and take a locally finite open refining cover V\mathcal V by [F2].

F2choose
2.1

Suppose V\mathcal V were infinite. For every nn the family of (n+1)(n+1)-element subsets of V\mathcal V is nonempty; [A1] chooses one EnE_n. Then E=nEnE=\bigcup_nE_n is at most countable by [L2] and infinite because it has finite subsets of arbitrarily large size. Hence, by the definition of at-most-countable, EE is countably infinite; enumerate its distinct members as (Vn)nN(V_n)_{n\in\mathbb N}.

A1L2step 1.1construct
3.1

By [A1] choose dnVnd_n\in V_n for every nn. The range D={dn:nN}D=\{d_n:n\in\mathbb N\} is infinite: if it were finite, local finiteness would make only finitely many distinct VnV_n meet DD, but every VnV_n contains dnDd_n\in D. Moreover the singleton family {{d}:dD}\{\{d\}:d\in D\} is locally finite, since a neighbourhood meeting only finitely many VnV_n can contain only finitely many points dDd\in D.

A1F2step 2.1construct
4.1

Hausdorffness makes points closed, so [L1] makes DD closed. For each dDd\in D, local finiteness gives a neighbourhood meeting only finitely many points of DD; pass to an open subneighbourhood and remove those finitely many other closed points. Using [A1] along an enumeration of DD yields open sets OdO_d with OdD={d}O_d\cap D=\{d\}.

A1F3L1step 3.1construct
5.1

The open set XDX\setminus D, together with the at most countable family {Od:dD}\{O_d:d\in D\}, is an open cover with no finite subcover, contradicting countable compactness in [F1].

F1step 3.1step 4.1
6.1

Hence V\mathcal V is finite. By [L3], select for each member of this finite refining family one containing member of U\mathcal U; the selected members form a finite subcover of U\mathcal U.

step 1.1step 5.1L3
7.1

Since U\mathcal U was arbitrary, [F1] proves that XX is compact.

F1step 6.1

Remarks

Countable choice is spent twice: first to extract a countably infinite subfamily from a putatively infinite locally finite cover, and then to choose one point from each member of that subfamily. The final selection is only finite choice, which is available in ZF.

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 104 results over 26 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