lift_iSup_le — Mathlib

English

If range f is bounded above and each lift(f(i)) ≤ t, then lift(iSup f) ≤ t.

Русский

Если диапазон f ограничен сверху и каждое lift(f(i)) ≤ t, то lift(iSup f) ≤ t.

LaTeX

$$$BddAbove(\mathrm{range}(f)) \land (\forall i, \text{lift}(f(i)) \le t) \Rightarrow \text{lift}(\iSup f) \le t$$$

Lean4

/-- To prove that the lift of a supremum is bounded by some cardinal `t`,
it suffices to show that the lift of each cardinal is bounded by `t`. -/
theorem lift_iSup_le {ι : Type v} {f : ι → Cardinal.{w}} {t : Cardinal} (hf : BddAbove (range f))
    (w : ∀ i, lift.{u} (f i) ≤ t) : lift.{u} (iSup f) ≤ t :=
  by
  rw [lift_iSup hf]
  exact ciSup_le' w

Похожие утверждения