English
Two well-orders have a smaller lifted type relation iff there exists a strict initial-segment embedding.
Русский
Пусть два хорошо упорядоченных множества имеют отношение меньшего поднятого типа тогда и только тогда, когда существует строгое вложение в начальный сегмент.
LaTeX
$$$\\text{lift}(\\mathrm{type}(r)) < \\text{lift}(\\mathrm{type}(s)) \\iff \\mathrm{Nonempty}(r \\prec_i s).$$$
Lean4
theorem lift_type_lt {α : Type u} {β : Type v} {r s} [IsWellOrder α r] [IsWellOrder β s] :
lift.{max v w} (type r) < lift.{max u w} (type s) ↔ Nonempty (r ≺i s) :=
by
constructor <;> refine fun ⟨f⟩ ↦ ⟨?_⟩
· exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r).symm).transInitial (RelIso.preimage Equiv.ulift s).toInitialSeg
· exact (f.relIsoTrans (RelIso.preimage Equiv.ulift r)).transInitial (RelIso.preimage Equiv.ulift s).symm.toInitialSeg
