DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-07-26 (claude-opus-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.
Initial segment of a well-order
Definition
Let be a well-order (Well-order and well-ordered set).
A subset is an initial segment of when it is downward closed: if and then . It is a proper initial segment when .
For write
and call the initial segment determined by .
Every initial segment , carrying the order inherited from , is itself a well-order: the inherited order is total, and a nonempty subset of is a nonempty subset of , so it has a least element, which lies in .
Remarks
- and are initial segments of ; each is a proper initial segment, since by irreflexivity; and each is an initial segment.
- Every proper initial segment is for exactly one . Let be an initial segment and put , which exists because is a nonempty subset of the well-order (Well-order and well-ordered set). If then by minimality of , so ; hence . Conversely let . Then , because , and is impossible, because downward closure would then put ; so by trichotomy, and . Therefore . For uniqueness, suppose with , say ; then , that is , which is impossible.
- Nesting. If then , so an initial segment of an initial segment of is an initial segment of . This is used whenever two well-orders are compared.
- The initial segments of are therefore exactly the sets for , together with itself, and inclusion orders them in the same shape as with one extra element added on top.
- The corresponding notion for a general poset would be a downward closed set, or "lower set". Nothing on this page needs it outside the well-ordered case, so the definition is stated only there, where the second clause above makes the family of initial segments completely explicit.