apply_liminf_iterate — Mathlib

English

Let f : α → α be a complete lattice endomorphism. Then the liminf of its iterates is fixed by f.

Русский

Пусть f : α → α — автоморфизм полной решетки. Тогда лиминф последовательности f^n(a) является фиксированной точкой f.

LaTeX

$$$ f\\left( \\liminf_{n} f^{[n]}(a) \\right) = \\liminf_{n} f^{[n]}(a) $$$

Lean4

/-- If `f : α → α` is a morphism of complete lattices, then the liminf of its iterates of any
`a : α` is a fixed point. -/
theorem _root_.CompleteLatticeHom.apply_liminf_iterate (f : CompleteLatticeHom α α) (a : α) :
    f (liminf (fun n => f^[n] a) atTop) = liminf (fun n => f^[n] a) atTop :=
  (CompleteLatticeHom.dual f).apply_limsup_iterate _

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