English
For any initial segment f, there exist γ,t such that IsWellOrder γ t and Nonempty (RelIso (Sum.Lex r t) s).
Русский
Для любого начального отрезка f существует γ,t с IsWellOrder γ t и Nonempty(RelIso (Sum.Lex r t) s).
LaTeX
$$$\\forall f:\\ InitialSeg\\ r\\ s,\\exists γ,\\exists t, IsWellOrder γ t \\land Nonempty (RelIso (Sum.Lex r t) s)$$$
Lean4
/-- An initial segment can be extended to an isomorphism by joining a second well order to the
domain. -/
theorem exists_sum_relIso {β : Type u} {s : β → β → Prop} [IsWellOrder β s] (f : r ≼i s) :
∃ (γ : Type u) (t : γ → γ → Prop), IsWellOrder γ t ∧ Nonempty (Sum.Lex r t ≃r s) := by
classical
obtain f | f := f.principalSumRelIso
· exact ⟨_, _, inferInstance, ⟨(RelIso.sumLexCongr f.subrelIso.symm (.refl _)).trans <| .sumLexComplLeft ..⟩⟩
· exact ⟨PEmpty, nofun, inferInstance, ⟨(RelIso.sumLexEmpty r _).trans f⟩⟩
