lift_aleph

Stream: lean4

[Nir Paz]

@Violeta Hernández Hey, do you have any advice on how to approach this?

theorem lift_aleph {o : Ordinal.{u}} : lift.{v, u} (aleph o) = aleph (lift.{v, u} o)

I don't know this part of the library well and I'm having trouble.

[Violeta Hernández]

I have an open PR proving this exact theorem!

[Violeta Hernández]

Basically, both maps are principal segment embeddings, and there can only be one between two given well orders

[Nir Paz]

Oh great! I'll take a look at it

[Violeta Hernández]

I actually give a proof using only transfinite recursion in #16306, but I'm waiting for #16220 to give the much shorter argument using principal segments.

[Violeta Hernández]

For posterity, docs#Cardinal.lift_aleph now exists.