LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Countable intersections of club subsets of omega_1 are club

Statement

Assume ${A C}_{ω}$ . If $C_{n} \subseteq ω_{1}$ is closed and unbounded for every $n \in N$ , then $⋂_{n} C_{n}$ is closed and unbounded in $ω_{1}$ .

Facts & Assumptions

Given: Each $C_{n}$ is closed and unbounded, and ${A C}_{ω}$ holds.

[L1]

Under ${A C}_{ω}$ , every countable subset of $ω_{1}$ is bounded below $ω_{1}$ . (Assuming countable choice: every at most countable subset of $ω_{1}$ is bounded below $ω_{1}$ , so no at most countable subset of $ω_{1}$ is cofinal in it, and a supremum of at most countably many at most countable ordinals is at most countable)

Proof

technique · diagonal construction

1.1L1

Finite intersections of clubs are club: closedness is immediate, and for two clubs one alternately chooses larger points in them; the supremum of the resulting omega-sequence is below $ω_{1}$ by [L1] and belongs to both by closedness. Induction handles finitely many.

2.1step 1.1L1

Given $α < ω_{1}$ , recursively choose $β_{k + 1} \in ⋂_{n \leq k} C_{n}$ with $β_{k + 1} > β_{k}$ , starting above $α$ ; step 1.1 supplies such a point. Let $δ = \sup_{k} β_{k} < ω_{1}$ by [L1]. For each fixed $n$ , the tail $(β_{k})_{k > n}$ lies in $C_{n}$ , so closedness gives $δ \in C_{n}$ . Also $δ > α$ .

3.1step 2.1∎

Thus the intersection is unbounded. It is closed as an arbitrary intersection of closed sets, hence is club.

Depends on

Used by

The Dieudonne club-set function is a Borel measure Theorem

Dependency tree · two levels

24 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

Donald L. Cohn, Measure Theory, 2nd ed., Chapter 7 (standard reference, not scraped)