[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
⊢ support (deriv f) ⊆ tsupport f
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ x ∈ support (deriv f) → x ∈ tsupport f
[PROOFSTEP]
rw [← not_imp_not]
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
⊢ ¬x ∈ tsupport f → ¬x ∈ support (deriv f)
[PROOFSTEP]
intro h2x
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h2x : ¬x ∈ tsupport f
⊢ ¬x ∈ support (deriv f)
[PROOFSTEP]
rw [not_mem_tsupport_iff_eventuallyEq] at h2x 
[GOAL]
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
E : Type v
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
h2x : f =ᶠ[nhds x] 0
⊢ ¬x ∈ support (deriv f)
[PROOFSTEP]
exact nmem_support.mpr (h2x.deriv_eq.trans (deriv_const x 0))
