LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

Continuous functions on [0, omega_1] are eventually constant

Statement

Assume ${A C}_{ω}$ . Every continuous $f : [0, ω_{1}] \to R$ or $C$ is constant on some terminal interval $[α, ω_{1}]$ .

Facts & Assumptions

Given: $f$ is continuous and ${A C}_{ω}$ holds.

[L1]

Under ${A C}_{ω}$ , a countable subset of $ω_{1}$ is bounded. (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 · direct

1.1given

For every $n \geq 1$ , continuity at $ω_{1}$ gives an ordinal $α_{n} < ω_{1}$ such that $∣ f (β) - f (ω_{1}) ∣ < 1 / n$ whenever $α_{n} < β \leq ω_{1}$ .

2.1step 1.1L1∎

By [L1], $α = \sup_{n} (α_{n} + 1) < ω_{1}$ . If $β \in [α, ω_{1}]$ , then the inequality in step 1.1 holds for every $n$ , so $f (β) = f (ω_{1})$ .

Depends on

Used by

The Dieudonne measure and top-point Dirac mass agree on continuous functions Lemma

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)