E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (z : ℂ) in 𝓝[{c}ᶜ] c, DifferentiableAt ℂ f z
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
rw [eventually_nhdsWithin_iff] at hd
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
have : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c}) := fun z hz =>
  (hz.1 hz.2).differentiableWithinAt
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
H : DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) {x | (fun x => x ∈ {c}ᶜ → DifferentiableAt ℂ f x) x}
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
have H := differentiableOn_update_limUnder_of_isLittleO hd this ho
no goals
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
hd : ∀ᶠ (x : ℂ) in 𝓝 c, x ∈ {c}ᶜ → DifferentiableAt ℂ f x
ho : (fun z => f z - f c) =o[𝓝[{c}ᶜ] c] fun z => (z - c)⁻¹
this : DifferentiableOn ℂ f ({z | z ≠ c → DifferentiableAt ℂ f z} \ {c})
H : DifferentiableOn ℂ (update f c (limUnder (𝓝[{c}ᶜ] c) f)) {x | (fun x => x ∈ {c}ᶜ → DifferentiableAt ℂ f x) x}
⊢ Tendsto f (𝓝[{c}ᶜ] c) (𝓝 (limUnder (𝓝[{c}ᶜ] c) f))
exact continuousAt_update_same.1 (H.differentiableAt hd).continuousAt