Definition·D054
Well order
A total order in which every nonempty subset has a least element.
A total order
on
is a well order when every nonempty subset has a least element:
The pair
is then a well-ordered set.
In words
For every S, if S is a nonempty subset of A then S has a least element.
Rests onA02
Never needed: F02 · F03 · F04 · F05 · F06 · F08 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Remarks
Well orders are the orders one can perform induction along. The well-ordering principle says the naturals under their usual order are well ordered, T18. The axiom of choice is equivalent to the statement that every set admits some well order (Zermelo's well-ordering theorem), not proved here. Well-ordered sets are the backbone of the ordinal numbers, each ordinal being the order type of a well order.