iSup_lt_lift — Mathlib

English

For any i, f i < c implies iSup f < c when appropriate cof bounds hold, with lift.

Русский

При условии подходящих ограничений cof и lift, если для всех i выполняется f(i) < c, то iSup f < c.

LaTeX

$$$\\forall {\\iota} {f}: {\\iota} \\to \\operatorname{Ordinal},\\ (\\forall i, \\operatorname{Ordinal}(f(i)) < c) \\Rightarrow \\operatorname{iSup}(f) < c.$$$

Lean4

theorem iSup_lt_lift {ι} {f : ι → Cardinal} {c : Cardinal} (hι : Cardinal.lift.{v, u} #ι < c.ord.cof)
    (hf : ∀ i, f i < c) : iSup f < c := by
  rw [← ord_lt_ord, iSup_ord]
  refine iSup_lt_ord_lift hι fun i => ?_
  rw [ord_lt_ord]
  apply hf

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