Cofinality results for indexed suprema

A more general universe version of iSup_lt_ord_lift and a related corollary phrased in terms of Iio.

theorem Ordinal.iSup_lt_ord_lift' {ι : Type v} {f : ι → Ordinal.{u}} {c : Ordinal.{u}} (hι : Cardinal.lift.{u, v} (Cardinal.mk ι) < Cardinal.lift.{v, u} c.cof) : (∀ (i : ι), f i < c) → iSup f < c

A version of lift_iSup_lt_of_lt_cof with more general universes.

theorem Ordinal.iSup_Iio_lt_ord {δ : Ordinal.{u}} {ℓ : Ordinal.{v}} {f : ↑(Set.Iio ℓ) → Ordinal.{u}} (hf : ∀ (i : ↑(Set.Iio ℓ)), f i < δ) (hcard : Cardinal.lift.{u, v} ℓ.card < Cardinal.lift.{v, u} δ.cof) : iSup f < δ