English
If cof(c) is large enough, and the index set is small, then the nfpFamily of f at a below c is below c, provided pointwise bounds hold.
Русский
Если cof(c) достаточно велико и индексное множество мало, то nfpFamily f a < c при a < c, если f(i,b) < c для всех i,b<c.
LaTeX
$$$\\text{(hc)}:\\aleph_0 < \\operatorname{cof}(c) \\quad \\text{and} \\quad \\operatorname{lift}(\\#\\iota) < \\operatorname{cof}(c) \\quad \\text{and} \\ \\forall i, \\forall b < c, f(i,b) < c \\Rightarrow \\forall a < c, \\operatorname{nfpFamily}(f,a) < c.$$$
Lean4
theorem nfpFamily_lt_ord_lift {ι} {f : ι → Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c)
(hc' : Cardinal.lift.{v, u} #ι < cof c) (hf : ∀ (i), ∀ b < c, f i b < c) {a} (ha : a < c) : nfpFamily f a < c :=
by
refine iSup_lt_ord_lift ((Cardinal.lift_le.2 (mk_list_le_max ι)).trans_lt ?_) fun l => ?_
· rw [lift_max]
apply max_lt _ hc'
rwa [Cardinal.lift_aleph0]
·
induction l with
| nil => exact ha
| cons i l H => exact hf _ _ H
