f g : CircleDeg1Lift
hf : Continuous ↑f
n : ℕ
⊢ Continuous (↑f^[n])
f g : CircleDeg1Lift
hf : Continuous ↑f
n : ℕ
⊢ Continuous ↑(f ^ n)
rw [coe_pow]
no goals
f g : CircleDeg1Lift
hf : Continuous ↑f
n : ℕ
⊢ Continuous (↑f^[n])
exact hf.iterate n