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.
Well-order and well-ordered set
Definition
Let be a set. A well-order on is a total order on (Partial order and partially ordered set) with the property that
The pair is then a well-ordered set, and is well-ordered by .
A least element of is unique when it exists: two of them are below each other, hence equal by antisymmetry (Partial order and partially ordered set). We may therefore write for it.
Strict form. Everything on this page is more convenient in terms of the associated strict order (Partial order and partially ordered set). Spelled out strictly, a well-order on is a relation that is
- irreflexive: holds for no ;
- transitive: and imply ;
- trichotomous: for all exactly one of , , holds;
- and such that every nonempty has an element with no satisfying .
The two presentations determine each other by or , and we write or as convenient.
Remarks
- Totality is not an extra hypothesis. If is a partial order on in which every nonempty subset has a least element, then is already total: apply the hypothesis to the two element subset , whose least element is below the other. Totality is nevertheless stated, because in the strict presentation trichotomy has to be written down explicitly.
- A well-order is total, so every subset of a well-ordered set is a chain (Chain in a poset), and itself is one. Chains are therefore not the interesting invariant here; the least element property is.
- The model case is , which is a linear order ( is a linear order on ) in which every nonempty subset has a least element (The well-ordering principle). Ordinals, defined later on this page, are the exact generalisation of that picture.
- and are total orders but not well-orders: has no least element at all, and the bounded set has none either. Being bounded below does not help, which is exactly why well-ordering is a strong condition.
- The empty set carries exactly one well-order, the empty relation, vacuously. Every one element set carries exactly one.
- A well-order admits no infinite strictly decreasing sequence , since the set of its terms would have no least element. This direction follows directly from the definition; no converse is used here.