𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ HasDerivAtFilter f f' x (𝓝 x ⊓ 𝓟 s) ↔ Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 ({x}ᶜ)) (𝓝 f')
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ HasDerivWithinAt f f' s x ↔ Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')
simp only [HasDerivWithinAt, nhdsWithin, diff_eq, inf_assoc.symm, inf_principal.symm]
no goals
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
E : Type w
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
⊢ HasDerivAtFilter f f' x (𝓝 x ⊓ 𝓟 s) ↔ Tendsto (slope f x) (𝓝 x ⊓ 𝓟 s ⊓ 𝓟 ({x}ᶜ)) (𝓝 f')
exact hasDerivAtFilter_iff_tendsto_slope