Lemma·L50
Trichotomy in a total order
In any totally ordered set, two elements compare one way, the other way, or are equal, and only one of those.
Let
be a total order. For
, exactly one of
holds.
In words
For any two elements of a totally ordered set, exactly one of three things holds: the first relates to the second and they differ, they are equal, or the second relates to the first and they differ.
Never needed: F05 · F09 · F10 · F11 · F12 · F13 · F14 · A01 · A03 · A04 · A05 · A06 · A07 · A08 (computed from the citation graph, not asserted).
Proof
- 1At least one. By excluded middle, or . If , the second holds. If : by comparability of D052, or ; combined with , this gives the first or the third.
- 2At most one. The first and second cannot both hold, since they assert and (negation); the second and third cannot both hold, symmetrically. The first and third cannot both hold: if and , antisymmetry (part of the underlying partial order) gives , contradicting .
∎
Remarks
The abstract form of trichotomy on the naturals, which D052's own commentary notes but does not prove; proved here once for every total order. Applied to
via T24, this underlies the sign case-analysis in L53.