English
Principal-segment version of the lift operation embeds Ordinal.u into Ordinal.max(u+1,v) as a principal segment.
Русский
Главная-сегментная версия операции подъёма встраивает Ordinal.u в Ordinal.max(u+1,v) как главный сегмент.
LaTeX
$$$\text{liftPrincipalSeg} : \text{Ordinal}^{u} \lt i \text{Ordinal}^{\max(u+1,v)}$$$
Lean4
/-- Principal segment version of the lift operation on ordinals, embedding `Ordinal.{u}` in
`Ordinal.{v}` as a principal segment when `u < v`. -/
def liftPrincipalSeg : Ordinal.{u} <i Ordinal.{max (u + 1) v} :=
⟨↑liftInitialSeg.{max (u + 1) v, u}, univ.{u, v},
by
refine fun b => inductionOn b ?_; intro β s _
rw [univ, ← lift_umax]; constructor <;> intro h
· obtain ⟨a, e⟩ := h
rw [← e]
refine inductionOn a ?_
intro α r _
exact lift_type_lt.{u, u + 1, max (u + 1) v}.2 ⟨typein r⟩
· rw [← lift_id (type s)] at h ⊢
obtain ⟨f⟩ := lift_type_lt.{_, _, v}.1 h
obtain ⟨f, a, hf⟩ := f
exists a
induction a using inductionOn with
| H a
r =>
refine
lift_type_eq.{u, max (u + 1) v, max (u + 1) v}.2
⟨(RelIso.ofSurjective (RelEmbedding.ofMonotone ?_ ?_) ?_).symm⟩
· exact fun b => enum r ⟨f b, (hf _).1 ⟨_, rfl⟩⟩
· refine fun a b h => (typein_lt_typein r).1 ?_
rw [typein_enum, typein_enum]
exact f.map_rel_iff.2 h
· intro a'
obtain ⟨b, e⟩ := (hf _).2 (typein_lt_type _ a')
exists b
simp only [RelEmbedding.ofMonotone_coe]
simp [e]⟩
