English
Two well-orders have equal lifted types if and only if they are isomorphic as well-orders.
Русский
У двух хорошо упорядоченных множеств равны поднимаемые типы тогда и только тогда, когда они изоморфны как хорошо упорядоченные.
LaTeX
$$$\\text{lift}(\\mathrm{type}(r)) = \\text{lift}(\\mathrm{type}(s)) \\iff \\mathrm{Nonempty}(r \\cong_r s).$$$
Lean4
theorem lift_type_eq {α : Type u} {β : Type v} {r s} [IsWellOrder α r] [IsWellOrder β s] :
lift.{max v w} (type r) = lift.{max u w} (type s) ↔ Nonempty (r ≃r s) :=
by
refine Quotient.eq'.trans ⟨?_, ?_⟩ <;> refine fun ⟨f⟩ ↦ ⟨?_⟩
· exact (RelIso.preimage Equiv.ulift r).symm.trans <| f.trans (RelIso.preimage Equiv.ulift s)
· exact (RelIso.preimage Equiv.ulift r).trans <| f.trans (RelIso.preimage Equiv.ulift s).symm
