E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
c p : ℝ
n : ℕ∞
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) Set.univ x
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
c p : ℝ
n : ℕ∞
m : ℕ
hf : ContDiffAt ℝ (↑m) f x
h : ↑m ≤ p
⊢ ContDiffAt ℝ (↑m) (fun x => f x ^ p) x
rw [← contDiffWithinAt_univ] at *
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f g : E → ℝ
f' g' : E →L[ℝ] ℝ
x : E
s : Set E
c p : ℝ
n : ℕ∞
m : ℕ
hf : ContDiffWithinAt ℝ (↑m) f Set.univ x
h : ↑m ≤ p
⊢ ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) Set.univ x
exact hf.rpow_const_of_le h