α : Type u_1
β : Type ?u.3017
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x
α : Type u_1
β : Type ?u.3017
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsPeriodicPt (f ∘ g) n x
rw [IsPeriodicPt, hco.comp_iterate]
no goals
α : Type u_1
β : Type ?u.3017
f fa : α → α
fb : β → β
x y : α
m n : ℕ
g : α → α
hco : Commute f g
hf : IsPeriodicPt f n x
hg : IsPeriodicPt g n x
⊢ IsFixedPt (f^[n] ∘ g^[n]) x
exact IsFixedPt.comp hf hg