[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ IsFixedPt f y
[PROOFSTEP]
refine' tendsto_nhds_unique ((tendsto_add_atTop_iff_nat 1).1 _) hy
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => f^[n + 1] x) atTop (𝓝 (f y))
[PROOFSTEP]
simp only [iterate_succ' f]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : T2Space α
f : α → α
x y : α
hy : Tendsto (fun n => f^[n] x) atTop (𝓝 y)
hf : ContinuousAt f y
⊢ Tendsto (fun n => (f ∘ f^[n]) x) atTop (𝓝 (f y))
[PROOFSTEP]
exact hf.tendsto.comp hy
