English
A variant of the previous lifting inequality with universes specialized to avoid unification issues: if hf, hf' bound the ranges and h relates f to f' via g with inequalities, then lift(iSup f) ≤ lift(iSup f').
Русский
Увариант неравенства подьема для iSup с конкретизацией вселенных; если hf и hf' ограничивают диапазоны, а h связывает f и f' через g и отношения неравенств, то lift(iSup f) ≤ lift(iSup f').
LaTeX
$$$BddAbove(\mathrm{range}(f)) \land BddAbove(\mathrm{range}(f')) \land (g : \iota \to \iota') \land (\forall i,\ lift(f(i)) \le lift(f'(g(i)))) \Rightarrow \ lift(\iSup f) \le lift(\iSup f')$$$
Lean4
/-- A variant of `lift_iSup_le_lift_iSup` with universes specialized via `w = v` and `w' = v'`.
This is sometimes necessary to avoid universe unification issues. -/
theorem lift_iSup_le_lift_iSup' {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{v}} {f' : ι' → Cardinal.{v'}}
(hf : BddAbove (range f)) (hf' : BddAbove (range f')) (g : ι → ι')
(h : ∀ i, lift.{v'} (f i) ≤ lift.{v} (f' (g i))) : lift.{v'} (iSup f) ≤ lift.{v} (iSup f') :=
lift_iSup_le_lift_iSup hf hf' h
