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.
Cofinal subset of an ordinal
Definition
Let be an ordinal (Ordinal (von Neumann)). A subset is cofinal in , equivalently unbounded in , when
A subset that is not cofinal is bounded below : there is such that for every .
Remarks
-
At a limit ordinal, cofinal means the supremum is attained from below. If is a limit ordinal (Successor and limit ordinals) and is nonempty, then is cofinal in if and only if (claim (e) of Basic closure properties of ordinals). If , then every lies in some , so and is cofinal. Conversely, if is cofinal then , because each satisfies by transitivity; and for the ordinal again lies in (Successor and limit ordinals), so cofinality supplies with , whence and , giving . This is the form in which the notion is used on this page, and it is exactly the hypothesis of the continuity clause of Monotonicity of ordinal and : strictly increasing and continuous in the right argument, weakly increasing in the left, with left cancellation, and the identities and .
-
At and at successors the notion is degenerate. is cofinal in , vacuously, and it is the only subset of . If then is the greatest element of (Basic closure properties of ordinals, Trichotomy and well-ordering of the ordinals), so a subset is cofinal in if and only if it contains . The interesting case is the limit case, and that is where the notion is used.
-
What is not defined at this point in the reading order. The cofinality , the least order type of a cofinal subset, and the vocabulary of regular and singular cardinals, are not introduced here; they are introduced later, on Cardinal Arithmetic, Cofinality and the Alephs. Nothing on this page needs them: the boundedness theorem below is stated as "no at most countable subset is cofinal", which is a statement about subsets and not about a cardinal invariant.
-
Cofinal is a property of the pair, not of the set. is cofinal in and bounded below . The ordinal must always be named.