English
If cof(c) > aleph0 and #ι < cof(c) and for all i, b < c, f(i,b) < c, then for all a < c, nfpFamily f a < c.
Русский
Если cof(c) > aleph0 и |ι| < cof(c), и для всех i, b < c, f(i,b) < c, тогда для всех a < c, nfpFamily f a < c.
LaTeX
$$$\\text{hc}: \\aleph_0 < \\operatorname{cof}(c) \\quad \\text{and} \\quad \\operatorname{hc'}: \\#ι < \\operatorname{cof}(c) \\quad \\text{and} \\quad \\forall i, \\forall b < c, f(i,b) < c \\Rightarrow \\forall a < c, \\operatorname{nfpFamily}(f,a) < c.$$$
Lean4
theorem nfpFamily_lt_ord {ι} {f : ι → Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hc' : #ι < cof c)
(hf : ∀ (i), ∀ b < c, f i b < c) {a} : a < c → nfpFamily.{u, u} f a < c :=
nfpFamily_lt_ord_lift hc (by rwa [(#ι).lift_id]) hf
