English
If f : α → α is a morphism of complete lattices and a ∈ α, then f(limsup (f^[n] a)) = limsup (f^[n] a).
Русский
Пусть f : α → α — морфизм полной решетки и a ∈ α. Тогда f(limsup (f^[n] a)) = limsup (f^[n] a).
LaTeX
$$$ f\\left( \\limsup_{n\\to\\infty} f^{[n]}(a) \\right) = \\limsup_{n\\to\\infty} f^{[n]}(a) $$$
Lean4
/-- If `f : α → α` is a morphism of complete lattices, then the limsup of its iterates of any
`a : α` is a fixed point. -/
@[simp]
theorem _root_.CompleteLatticeHom.apply_limsup_iterate (f : CompleteLatticeHom α α) (a : α) :
f (limsup (fun n => f^[n] a) atTop) = limsup (fun n => f^[n] a) atTop :=
by
rw [limsup_eq_iInf_iSup_of_nat', map_iInf]
simp_rw [_root_.map_iSup, ← Function.comp_apply (f := f), ← Function.iterate_succ' f, ← Nat.add_succ]
conv_rhs => rw [iInf_split _ (0 < ·)]
simp only [not_lt, Nat.le_zero, iInf_iInf_eq_left, add_zero, iInf_nat_gt_zero_eq, left_eq_inf]
refine (iInf_le (fun i => ⨆ j, f^[j + (i + 1)] a) 0).trans ?_
simp only [zero_add, iSup_le_iff]
exact fun i => le_iSup (fun i => f^[i] a) (i + 1)
