cof_lsub_le_lift — Mathlib

English

For any f, cof(lsub(f)) ≤ lift(#ι).

Русский

Для любой функции f: cof(lsub(f)) ≤ lift(|ι|).

LaTeX

$$$\\operatorname{cof}(\\operatorname{lsub}(f)) \\le \\operatorname{lift}(\\#\\iota).$$$

Lean4

theorem cof_lsub_le_lift {ι} (f : ι → Ordinal) : cof (lsub.{u, v} f) ≤ Cardinal.lift.{v, u} #ι :=
  by
  rw [← mk_uLift.{u, v}]
  convert cof_lsub_le.{max u v} fun i : ULift.{v, u} ι => f i.down
  exact
    lsub_eq_of_range_eq.{u, max u v, max u v}
      (Set.ext fun x => ⟨fun ⟨i, hi⟩ => ⟨ULift.up.{v, u} i, hi⟩, fun ⟨i, hi⟩ => ⟨_, hi⟩⟩)

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