E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.251275
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_1
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x✝² y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), fderiv 𝕜 f x = 0
x✝¹ y x : E
x✝ : x ∈ univ
⊢ fderiv 𝕜 f x = 0
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.251275
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_1
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x✝² y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), fderiv 𝕜 f x = 0
x✝¹ y x : E
x✝ : x ∈ univ
⊢ fderivWithin 𝕜 f univ x = 0
rw [fderivWithin_univ]
no goals
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
F : Type ?u.251275
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℝ F
𝕜 : Type u_1
G : Type u_3
inst✝³ : IsROrC 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
C : ℝ
s : Set E
x✝² y✝ : E
f' g' : E → E →L[𝕜] G
φ : E →L[𝕜] G
hf : Differentiable 𝕜 f
hf' : ∀ (x : E), fderiv 𝕜 f x = 0
x✝¹ y x : E
x✝ : x ∈ univ
⊢ fderiv 𝕜 f x = 0
exact hf' x