English
The lift operation forms an initial segment of cardinals across universes.
Русский
Операция lift образует начальный отрезок кардиналов между вселенными.
LaTeX
$$$$ \\text{liftInitialSeg} : \\mathrm{Cardinal} \\le_i \\mathrm{Cardinal}. $$$$
Lean4
/-- `Cardinal.lift` as an `InitialSeg`. -/
@[simps!]
def liftInitialSeg : Cardinal.{u} ≤i Cardinal.{max u v} :=
by
refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩ <;> intro a b
· refine inductionOn₂ a b fun _ _ ↦ ?_
rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]
· refine inductionOn₂ a b fun α β h ↦ ?_
obtain ⟨e⟩ := h.le
replace e := e.congr (Equiv.refl β) Equiv.ulift
refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
apply (e.codRestrict _ mem_range_self).equivOfSurjective
rintro ⟨a, ⟨b, rfl⟩⟩
exact ⟨b, rfl⟩
