English
Let hc be IsRegular c and hι: #ι < c. If hf gives f i b < c.ord for all i and b < c.ord, then for all a < c.ord, derivFamily f a < c.ord.
Русский
Пусть hc:IsRegular c и hι: #ι < c. Тогда если hf обеспечивает f i b < c.ord для всех i и b < c.ord, то derivFamily f a < c.ord для каждого a < c.ord.
LaTeX
$$$IsRegular(c) \land \#ι < c \Rightarrow ( \forall i, \forall b < \operatorname{ord}(c),\ f(i,b) < \operatorname{ord}(c) ) \Rightarrow \forall a < \operatorname{ord}(c),\operatorname{derivFamily}(f,a) < \operatorname{ord}(c)$$$
Lean4
theorem derivFamily_lt_ord {ι} {f : ι → Ordinal → Ordinal} {c} (hc : IsRegular c) (hι : #ι < c) (hc' : c ≠ ℵ₀)
(hf : ∀ (i), ∀ b < c.ord, f i b < c.ord) {a} : a < c.ord → derivFamily.{u, u} f a < c.ord :=
derivFamily_lt_ord_lift hc (by rwa [lift_id]) hc' hf
