nfp_lt_ord_of_isRegular — Mathlib

English

Let f be a function with f(i) < c for all i, where c is regular and aleph0 ≠ c. Then for every a < c.ord, nfp f a < c.ord.

Русский

Пусть f(i) < c для всех i, где c — регулярное и c ≠ aleph0. Тогда для каждого a < c.ord, nfp f a < c.ord.

LaTeX

$$$IsRegular(c) \land \ Ne(c, \aleph_0) \Rightarrow ( \forall i, f(i) < c ) \Rightarrow \forall a,\ a < \operatorname{ord}(c) \Rightarrow \operatorname{nfp}(f,a) < \operatorname{ord}(c)$$$

Lean4

theorem nfp_lt_ord_of_isRegular {f : Ordinal → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀)
    (hf : ∀ i < c.ord, f i < c.ord) {a} : a < c.ord → nfp f a < c.ord :=
  nfp_lt_ord (by rw [hc.cof_eq]; exact lt_of_le_of_ne hc.1 hc'.symm) hf

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