𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ f =ᶠ[𝓝 x] 0 → fderiv 𝕜 f x = 0
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ x ∈ support (fderiv 𝕜 f) → x ∈ tsupport f
rw [← not_imp_not, not_mem_tsupport_iff_eventuallyEq, nmem_support]
no goals
𝕜 : Type u_3
E : Type u_1
F : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
⊢ f =ᶠ[𝓝 x] 0 → fderiv 𝕜 f x = 0
exact fun hx => hx.fderiv_eq.trans <| fderiv_const_apply 0