English
There exists a case distinction: either there is an empty extension or there exists a sum lexicographic isomorphism; i.e., a sum-relIso exists.
Русский
Существует разделение на случаи: либо пустое продолжение, либо существует лексикографическое изоморфизм через сумму; существует RelIso для суммы и лексикографического порядка.
LaTeX
$$$\\exists γ,\\exists t, IsWellOrder\\ γ t \\land Nonempty (RelIso (Sum.Lex\\ r\\ t) s)$$$
Lean4
/-- Every initial segment embedding into a well order can be turned into an isomorphism if
surjective, or into a principal segment embedding if not. -/
noncomputable def principalSumRelIso [IsWellOrder β s] (f : r ≼i s) : (r ≺i s) ⊕ (r ≃r s) :=
if h : Surjective f then Sum.inr (RelIso.ofSurjective f h) else Sum.inl (f.toPrincipalSeg h)
