Lifting suprema of ordinals

Ordinal.lift commutes with the supremum of a family of ordinals bounded above, as Cardinal.lift_iSup does for cardinals.

Main results

• TauCeti.Ordinal.lift_iSup: the lift of a bounded supremum is the supremum of the lifts.

theorem TauCeti.Ordinal.lift_iSup {β : Type w} {f : β → Ordinal.{u}} (hf : BddAbove (Set.range f)) : Ordinal.lift.{v, u} (⨆ (i : β), f i) = ⨆ (i : β), Ordinal.lift.{v, u} (f i)

Ordinal.lift commutes with a bounded supremum: the lift of the supremum of a family of ordinals bounded above is the supremum of the lifts.