English
If two bounded families of cardinals f and f' are connected by a mapping g: I → I' such that for every i we have lift(f(i)) ≤ lift(f'(g(i))), then lift(iSup f) ≤ lift(iSup f').
Русский
Пусть имеются ограниченные семейства кардиналов f и f' с отображением g: I → I'. Если для каждого i выполняется lift(f(i)) ≤ lift(f'(g(i))), тогда lift( sup_i f(i) ) ≤ lift( sup_j f'(j) ).
LaTeX
$$$BddAbove(\mathrm{range}(f)) \land BddAbove(\mathrm{range}(f')) \land (\forall i,\ lift(f(i)) \le lift(f'(g(i)))) \Rightarrow \ lift(\iSup f) \le lift(\iSup f')$$$
Lean4
/-- To prove an inequality between the lifts to a common universe of two different supremums,
it suffices to show that the lift of each cardinal from the smaller supremum
if bounded by the lift of some cardinal from the larger supremum.
-/
theorem lift_iSup_le_lift_iSup {ι : Type v} {ι' : Type v'} {f : ι → Cardinal.{w}} {f' : ι' → Cardinal.{w'}}
(hf : BddAbove (range f)) (hf' : BddAbove (range f')) {g : ι → ι'}
(h : ∀ i, lift.{w'} (f i) ≤ lift.{w} (f' (g i))) : lift.{w'} (iSup f) ≤ lift.{w} (iSup f') :=
by
rw [lift_iSup hf, lift_iSup hf']
exact ciSup_mono' (bddAbove_range_comp.{_, _, w} hf' _) fun i => ⟨_, h i⟩
