English
Let c be regular, 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.
Русский
Пусть 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 \land \left( \forall i, \forall b < \operatorname{ord}(c),\ f(i,b) < \operatorname{ord}(c) \right) \Rightarrow \forall a < \operatorname{ord}(c),\operatorname{nfpFamily}(f,a) < \operatorname{ord}(c)$$$
Lean4
theorem nfpFamily_lt_ord_lift_of_isRegular {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c)
(hι : Cardinal.lift.{v, u} #ι < c) (hc' : c ≠ ℵ₀) (hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a} (ha : a < c.ord) :
nfpFamily f a < c.ord := by
apply nfpFamily_lt_ord_lift _ _ hf ha <;> rw [hc.cof_eq]
· exact lt_of_le_of_ne hc.1 hc'.symm
· exact hι
