English
Same as above: the intersection of fixed points over i is not bounded above.
Русский
То же самое: пересечение фиксированных точек по i не ограничено сверху.
LaTeX
$$$[Small.{u} ι] (H : ∀ i, IsNormal (f i)) : \\neg BddAbove (⋂ i, Function.fixedPoints (f i))$$
Lean4
/-- The derivative of a family of normal functions is the sequence of their common fixed points.
This is defined for all functions such that `Ordinal.derivFamily_zero`,
`Ordinal.derivFamily_succ`, and `Ordinal.derivFamily_limit` are satisfied. -/
def derivFamily (f : ι → Ordinal.{u} → Ordinal.{u}) (o : Ordinal.{u}) : Ordinal.{u} :=
limitRecOn o (nfpFamily f 0) (fun _ IH => nfpFamily f (succ IH)) fun a _ g => ⨆ b : Set.Iio a, g _ b.2
