English
If c is regular and c ≠ aleph0, and hf: ∀ i < c.ord, f i < c.ord, then for all a < c.ord, deriv f a < c.ord.
Русский
Если c регулярное и c ≠ aleph0, и hf: ∀ i < c.ord, f i < c.ord, то для любого a < c.ord, deriv f a < c.ord.
LaTeX
$$$IsRegular(c) \land c \neq \aleph_0 \Rightarrow ( \forall i < \operatorname{ord}(c),\ f(i) < \operatorname{ord}(c) ) \Rightarrow \forall a < \operatorname{ord}(c),\operatorname{deriv}(f,a) < \operatorname{ord}(c)$$$
Lean4
theorem deriv_lt_ord {f : Ordinal.{u} → Ordinal} {c} (hc : IsRegular c) (hc' : c ≠ ℵ₀) (hf : ∀ i < c.ord, f i < c.ord)
{a} : a < c.ord → deriv f a < c.ord :=
derivFamily_lt_ord_lift hc (by simpa using Cardinal.one_lt_aleph0.trans (lt_of_le_of_ne hc.1 hc'.symm)) hc' fun _ =>
hf
