𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b ↔ DifferentiableWithinAt 𝕜 f s b
refine' ⟨DifferentiableWithinAt.of_dslope, fun hd => _⟩
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ dslope f a =ᶠ[𝓝[s] b] fun y => (id y - a)⁻¹ • (f y - f a)
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ DifferentiableWithinAt 𝕜 (dslope f a) s b
refine' (((differentiableWithinAt_id.sub_const a).inv (sub_ne_zero.2 h)).smul
  (hd.sub_const (f a))).congr_of_eventuallyEq _ (dslope_of_ne _ h)
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ {a}ᶜ ∈ 𝓝[s] b
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ dslope f a =ᶠ[𝓝[s] b] fun y => (id y - a)⁻¹ • (f y - f a)
refine' (eqOn_dslope_slope _ _).eventuallyEq_of_mem _
no goals
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
hd : DifferentiableWithinAt 𝕜 f s b
⊢ {a}ᶜ ∈ 𝓝[s] b
exact mem_nhdsWithin_of_mem_nhds (isOpen_ne.mem_nhds h)