lsub_lt_ord_lift — Mathlib

English

If lift(#ι) < cof(c) and ∀ i, f(i) < c, then lsub(f) < c.

Русский

Если lift(|ι|) < cof(c) и для всех i верно f(i) < c, тогда lsub(f) < c.

LaTeX

$$$\\big( \\operatorname{lift}(\\#\\iota) < \\operatorname{cof}(c) \\big) \\Rightarrow \\big( \\forall i, f(i) < c \\big) \\Rightarrow \\operatorname{lsub}(f) < c.$$$

Lean4

theorem lsub_lt_ord_lift {ι} {f : ι → Ordinal} {c : Ordinal} (hι : Cardinal.lift.{v, u} #ι < c.cof)
    (hf : ∀ i, f i < c) : lsub.{u, v} f < c :=
  lt_of_le_of_ne (lsub_le hf) fun h => by
    subst h
    exact (cof_lsub_le_lift.{u, v} f).not_gt hι

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