nfp_lt_ord — Mathlib

English

There exists a function f on all a less than cof(o).ord such that blsub o f = o.

Русский

Существует функция f на всех a < cof(o).ord такая, что blsub o f = o.

LaTeX

$$$\\ exists\\ f:\\forall a< (\\operatorname{cof}(o)).ord, \\operatorname{Ordinal},\\ blsub(o,f)=o.$$$

Lean4

theorem nfp_lt_ord {f : Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hf : ∀ i < c, f i < c) {a} : a < c → nfp f a < c :=
  nfpFamily_lt_ord_lift hc (by simpa using Cardinal.one_lt_aleph0.trans hc) fun _ => hf

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