English
An initial-segment version of lifting embeds ordinals as an initial segment when u ≤ v.
Русский
Версия подъёма как начального сегмента внедряет ординалы в начальный сегмент при условии u ≤ v.
LaTeX
$$$\\text{liftInitialSeg}: \\mathrm{Ordinal}.(v) \\le_i \\mathrm{Ordinal}.({\\max(u,v)})$ and related construction.$$
Lean4
/-- Initial segment version of the lift operation on ordinals, embedding `Ordinal.{u}` in
`Ordinal.{v}` as an initial segment when `u ≤ v`. -/
def liftInitialSeg : Ordinal.{v} ≤i Ordinal.{max u v} :=
by
refine ⟨RelEmbedding.ofMonotone lift.{u} (by simp), fun a b ↦ Ordinal.inductionOn₂ a b fun α r _ β s _ h ↦ ?_⟩
rw [RelEmbedding.ofMonotone_coe, ← lift_id'.{max u v} (type s), ← lift_umax.{v, u}, lift_type_lt] at h
obtain ⟨f⟩ := h
use typein r f.top
rw [RelEmbedding.ofMonotone_coe, ← lift_umax, lift_typein_top, lift_id']
