English
Let (f i) be a family of cardinals indexed by i in I, with a bound above for the range of f. Then the lifted supremum satisfies lift(iSup f) ≤ t if and only if every lifted f(i) satisfies lift(f(i)) ≤ t.
Русский
Пусть существует семейство кардиналов f(i), индексируемое i из множества I, такое что диапазон значений ограничен сверху. Тогда при подъемe в одну вселенную: lift(iSup f) ≤ t тогда и только если для каждого i выполняется lift(f(i)) ≤ t.
LaTeX
$$$BddAbove(\mathrm{range}(f)) \Rightarrow \left( \lift(\iSup f) \le t \iff \forall i,\ \lift(f(i)) \le t \right)$$$
Lean4
@[simp]
theorem lift_iSup_le_iff {ι : Type v} {f : ι → Cardinal.{w}} (hf : BddAbove (range f)) {t : Cardinal} :
lift.{u} (iSup f) ≤ t ↔ ∀ i, lift.{u} (f i) ≤ t :=
by
rw [lift_iSup hf]
exact ciSup_le_iff' (bddAbove_range_comp.{_, _, u} hf _)
