α : Type u_1
β : Type ?u.950
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x
α : Type u_1
β : Type ?u.950
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsPeriodicPt f (n + m) x
rw [IsPeriodicPt, iterate_add]
no goals
α : Type u_1
β : Type ?u.950
f fa : α → α
fb : β → β
x y : α
m n : ℕ
hn : IsPeriodicPt f n x
hm : IsPeriodicPt f m x
⊢ IsFixedPt (f^[n] ∘ f^[m]) x
exact hn.comp hm