English
The relation between lifts of types corresponds to embeddability by initial segments.
Русский
Соотношение подъёмов типов соответствует вложениям по начальному сегменту.
LaTeX
$$$\\text{lift}(\\mathrm{type}(r)) \\le \\text{lift}(\\mathrm{type}(s)) \\iff \\mathrm{Nonempty}(r \\preccurlyeq_i s).$$$
Lean4
theorem lift_type_le {α : 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 (RelIso.preimage Equiv.ulift r).symm.toInitialSeg.trans (f.trans (RelIso.preimage Equiv.ulift s).toInitialSeg)
· exact (RelIso.preimage Equiv.ulift r).toInitialSeg.trans (f.trans (RelIso.preimage Equiv.ulift s).symm.toInitialSeg)
