English
For any two well orders r on α and s on β, either r ≼i s or s ≼i r holds; i.e., initial-segment comparison is total.
Русский
Для любых двух хорошо упорядоченных отношений r и s выполняется либо r ≼i s, либо s ≼i r.
LaTeX
$$$(r \\preccurlyeq_i s) \\oplus (s \\preccurlyeq_i r)$$$
Lean4
/-- For any two well orders, one is an initial segment of the other. -/
noncomputable def total (r s) [IsWellOrder α r] [IsWellOrder β s] : (r ≼i s) ⊕ (s ≼i r) :=
match (leAdd r s).principalSumRelIso, (RelEmbedding.sumLexInr r s).collapse.principalSumRelIso with
| Sum.inl f, Sum.inr g => Sum.inl <| f.transRelIso g.symm
| Sum.inr f, Sum.inl g => Sum.inr <| g.transRelIso f.symm
| Sum.inr f, Sum.inr g => Sum.inl <| (f.trans g.symm).toInitialSeg
| Sum.inl f, Sum.inl g =>
Classical.choice <| by
obtain h | h | h := trichotomous_of (Sum.Lex r s) f.top g.top
·
exact
⟨Sum.inl <|
(f.codRestrict {x | Sum.Lex r s x g.top} (fun a => _root_.trans (f.lt_top a) h) h).transRelIso
g.subrelIso⟩
· let f := f.subrelIso
rw [h] at f
exact ⟨Sum.inl <| (f.symm.trans g.subrelIso).toInitialSeg⟩
·
exact
⟨Sum.inr <|
(g.codRestrict {x | Sum.Lex r s x f.top} (fun a => _root_.trans (g.lt_top a) h) h).transRelIso
f.subrelIso⟩
