no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x : α
n : ℕ
⊢ Continuous fun a => a ^ Int.ofNat n
simpa using continuous_pow n
no goals
α : Type u
β : Type v
G : Type w
H : Type x
inst✝³ : TopologicalSpace G
inst✝² : Group G
inst✝¹ : TopologicalGroup G
inst✝ : TopologicalSpace α
f : α → G
s : Set α
x : α
n : ℕ
⊢ Continuous fun a => a ^ Int.negSucc n
simpa using (continuous_pow (n + 1)).inv