f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hg : HasDerivWithinAt g g' Set.univ x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivAt f f' x
hg : HasDerivAt g g' x
h : 0 < f x
⊢ HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
rw [← hasDerivWithinAt_univ] at *
no goals
f g : ℝ → ℝ
f' g' x y p : ℝ
s : Set ℝ
hf : HasDerivWithinAt f f' Set.univ x
hg : HasDerivWithinAt g g' Set.univ x
h : 0 < f x
⊢ HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) Set.univ x
exact hf.rpow hg h