English
For a fixed index i with f_i normal, applying f_i to the derivative does not change it: f_i(derivFamily f o) = derivFamily f o for all o.
Русский
Для заданного i, если f_i нормальная, то f_i(derivFamily f o) = derivFamily f o для всех o.
LaTeX
$$$$ f_i(derivFamily f o) = derivFamily f o. $$$$
Lean4
theorem derivFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (o : Ordinal) : f i (derivFamily f o) = derivFamily f o :=
by
induction o using limitRecOn with
| zero =>
rw [derivFamily_zero]
exact nfpFamily_fp H 0
| succ =>
rw [derivFamily_succ]
exact nfpFamily_fp H _
| limit o l IH =>
have := l.nonempty_Iio.to_subtype
rw [derivFamily_limit _ l, H.map_iSup]
refine eq_of_forall_ge_iff fun c => ?_
rw [Ordinal.iSup_le_iff, Ordinal.iSup_le_iff]
refine forall_congr' fun a ↦ ?_
rw [IH _ a.2]
