English
For a small index set, the derivative family equals the enumeration of the intersection of fixed points of all f_i.
Русский
Для малого множества индексов производная семейства равна перечислению пересечения фиксированных точек всех функций f_i.
LaTeX
$$$$ \derivFamily f = \operatorname{enumOrd}\Bigl( \bigcap_i \operatorname{fixedPoints}(f_i) \Bigr). $$$$
Lean4
/-- For a family of normal functions, `Ordinal.derivFamily` enumerates the common fixed points. -/
theorem derivFamily_eq_enumOrd [Small.{u} ι] (H : ∀ i, IsNormal (f i)) :
derivFamily f = enumOrd (⋂ i, Function.fixedPoints (f i)) :=
by
rw [eq_comm, eq_enumOrd _ (not_bddAbove_fp_family H)]
use (isNormal_derivFamily f).strictMono
rw [Set.range_eq_iff]
refine ⟨?_, fun a ha => ?_⟩
· rintro a S ⟨i, hi⟩
rw [← hi]
exact derivFamily_fp (H i) a
rw [Set.mem_iInter] at ha
rwa [← fp_iff_derivFamily H]
