cof_iSup_le — Mathlib

English

If ∀ i, f(i) < iSup f then cof(iSup f) ≤ #ι.

Русский

Если для всех i выполняется f(i) < iSup f, то cof(iSup f) ≤ #ι.

LaTeX

$$$\\forall {\\iota} {f}: {\\iota} \\to \\operatorname{Ordinal},\\ \\big( \\forall i, f(i) < \\operatorname{iSup}(f) \\big) \\Rightarrow \\operatorname{cof}(\\operatorname{iSup}(f)) \\le \\#\\iota.$$$

Lean4

theorem cof_iSup_le {ι} {f : ι → Ordinal} (H : ∀ i, f i < iSup f) : cof (iSup f) ≤ #ι :=
  by
  rw [← (#ι).lift_id]
  exact cof_iSup_le_lift H

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