not_bddAbove_fp — Mathlib

English

If f is normal, the set of fixed points of f is unbounded above.

Русский

Если f нормальна, множество фиксированных точек f не ограничено сверху.

LaTeX

$$$$ \neg BddAbove(\operatorname{fixedPoints} f). $$$$

Lean4

/-- The fixed point lemma for normal functions: any normal function has an unbounded set of
fixed points. -/
theorem not_bddAbove_fp (H : IsNormal f) : ¬BddAbove (Function.fixedPoints f) :=
  by
  convert not_bddAbove_fp_family fun _ : Unit => H
  exact (Set.iInter_const _).symm

Похожие утверждения