English
Let hc be IsRegular c, hι lift(#ι) < c, and hf: ∀ i, ∀ b < c.ord, f i b < c.ord. Then for every a < c.ord, nfpFamily f a < c.ord.
Русский
Пусть hc: IsRegular(c), hι: lift(#ι) < c, hf: ∀ i, ∀ b < c.ord, f i b < c.ord. Тогда для всякого a < c.ord, nfpFamily f a < c.ord.
LaTeX
$$$IsRegular(c) \land \operatorname{lift}(\#ι) < c \Rightarrow ( \forall i, \forall b < \operatorname{ord}(c),\ f(i,b) < \operatorname{ord}(c) ) \Rightarrow \forall a < \operatorname{ord}(c),\operatorname{nfpFamily}(f,a) < \operatorname{ord}(c)$$$
Lean4
theorem nfpFamily_lt_ord_of_isRegular {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c)
(hc' : c ≠ ℵ₀) {a} (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) : a < c.ord → nfpFamily.{u, u} f a < c.ord :=
nfpFamily_lt_ord_lift_of_isRegular hc (by rwa [lift_id]) hc' hf
