α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ n
α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ ↑n
simp_rw [zpow_ofNat]
no goals
α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ n
exact hf.pow_const _
α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => (f x ^ (n + 1))⁻¹
α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ Int.negSucc n
simp_rw [zpow_negSucc]
no goals
α : Type u_2
β : Type u_1
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => (f x ^ (n + 1))⁻¹
exact (hf.pow_const _).inv