English
For Small ι and IsNormal f_i, the intersection of fixed points is unbounded above; i.e., not BddAbove (⋂ i, fixedPoints (f i)).
Русский
Для малого ι и нормальных f_i пересечение фиксированных точек не ограничено сверху.
LaTeX
$$$[Small.{u} ι] (H : ∀ i, IsNormal (f i)) : \\neg BddAbove (⋂ i, Function.fixedPoints (f i))$$
Lean4
/-- A generalization of the fixed point lemma for normal functions: any family of normal functions
has an unbounded set of common fixed points. -/
theorem not_bddAbove_fp_family [Small.{u} ι] (H : ∀ i, IsNormal (f i)) : ¬BddAbove (⋂ i, Function.fixedPoints (f i)) :=
by
rw [not_bddAbove_iff]
refine fun a ↦ ⟨nfpFamily f (succ a), ?_, (lt_succ a).trans_le (le_nfpFamily f _)⟩
rintro _ ⟨i, rfl⟩
exact nfpFamily_fp (H i) _
