ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>y : E<GOAL>HasFDerivWithinAt f f' (s \ {y}) x ↔ HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>(fun p => f p.1 - f p.2) =O[𝓝 (x, x)] fun p => p.1 - p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>h : HasFDerivAtFilter f f' x L<GOAL>(fun x' => f x' - f x) =O[L] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<VAR>K : ℝ≥0<VAR>hK : ‖f'‖₊ < K<GOAL>∃ s ∈ 𝓝 x, LipschitzOnWith K f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>∃ K, ∃ s ∈ 𝓝 x, LipschitzOnWith K f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>v : E<VAR>α : Type u_6<VAR>c : α → 𝕜<VAR>l : Filter α<VAR>hc : Filter.Tendsto (fun n => ‖c n‖) l Filter.atTop<GOAL>Filter.Tendsto (fun n => c n • (f (x + (c n)⁻¹ • v) - f x)) l (𝓝 (f' v))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f₀' f₁' : E →L[𝕜] F<VAR>x : E<VAR>h₀ : HasFDerivAt f f₀' x<VAR>h₁ : HasFDerivAt f f₁' x<GOAL>f₀' = f₁'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>h : t ∈ 𝓝[s] x<GOAL>HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>h : t ∈ 𝓝 x<GOAL>HasFDerivWithinAt f f' (s ∩ t) x ↔ HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>hs : HasFDerivWithinAt f f' s x<VAR>ht : HasFDerivWithinAt f f' t x<GOAL>HasFDerivWithinAt f f' (s ∪ t) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hs : s ∈ 𝓝 x<GOAL>HasFDerivAt f f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>hs : s ∈ 𝓝 x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : 𝓝[s \ {x}] x = ⊥<GOAL>HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : x ∉ closure s<GOAL>HasFDerivWithinAt f f' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<GOAL>HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : DifferentiableAt 𝕜 f x<GOAL>HasFDerivAt f (fderiv 𝕜 f x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜 f s<VAR>hs : s ∈ 𝓝 x<GOAL>HasFDerivAt f (fderiv 𝕜 f x) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜 f s<VAR>hs : s ∈ 𝓝 x<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜 f s<VAR>hs : s ∈ 𝓝 x<GOAL>∀ᶠ (y : E) in 𝓝 x, DifferentiableAt 𝕜 f y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<GOAL>fderiv 𝕜 f x = f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E → E →L[𝕜] F<VAR>h : ∀ (x : E), HasFDerivAt f (f' x) x<GOAL>fderiv 𝕜 f = f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖fderiv 𝕜 f x₀‖ ≤ C
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x₀ : E<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖fderiv 𝕜 f x₀‖ ≤ ↑C
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖fderiv 𝕜 f x₀‖ ≤ ↑C
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 f s x = f'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>h : DifferentiableWithinAt 𝕜 f t x<VAR>st : s ⊆ t<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>t : Set E<VAR>hst : s ∈ 𝓝[t] x<GOAL>DifferentiableWithinAt 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<GOAL>DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>ht : t ∈ 𝓝 x<GOAL>DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>ht : t ∈ 𝓝[s] x<GOAL>DifferentiableWithinAt 𝕜 f (s ∩ t) x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableAt 𝕜 f x<GOAL>DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : Differentiable 𝕜 f<GOAL>DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableAt 𝕜 f x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 f s x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s t : Set E<VAR>h : DifferentiableOn 𝕜 f t<VAR>st : s ⊆ t<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>DifferentiableOn 𝕜 f Set.univ ↔ Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : Differentiable 𝕜 f<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : ∀ x ∈ s, ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)<GOAL>DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>st : t ∈ 𝓝[s] x<VAR>ht : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableWithinAt 𝕜 f t x<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>st : s ⊆ t<VAR>ht : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableWithinAt 𝕜 f t x<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>ht : t ∈ 𝓝 x<GOAL>fderivWithin 𝕜 f (s ∩ t) x = fderivWithin 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<GOAL>fderivWithin 𝕜 f Set.univ = fderiv 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : s ∈ 𝓝 x<GOAL>fderivWithin 𝕜 f s x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>hs : IsOpen s<VAR>hx : x ∈ s<GOAL>fderivWithin 𝕜 f s x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableAt 𝕜 f x<GOAL>fderivWithin 𝕜 f s x = fderiv 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set (E →L[𝕜] F)<VAR>x : E<GOAL>fderiv 𝕜 f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ fderiv 𝕜 f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>t : Set E<VAR>s : Set (E →L[𝕜] F)<VAR>x : E<GOAL>fderivWithin 𝕜 f t x ∈ s ↔ DifferentiableWithinAt 𝕜 f t x ∧ fderivWithin 𝕜 f t x ∈ s ∨ ¬DifferentiableWithinAt 𝕜 f t x ∧ 0 ∈ s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x₀ : E<VAR>n : ℕ<VAR>h : f =O[𝓝[s] x₀] fun x => ‖x - x₀‖ ^ n<VAR>hx₀ : x₀ ∈ s<VAR>hn : 1 < n<GOAL>HasFDerivWithinAt f 0 s x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x₀ : E<VAR>n : ℕ<VAR>h : f =O[𝓝 x₀] fun x => ‖x - x₀‖ ^ n<VAR>hn : 1 < n<GOAL>HasFDerivAt f 0 x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x₀ : E<VAR>f' : E →L[𝕜] F<VAR>h : HasFDerivWithinAt f f' s x₀<GOAL>(fun x => f x - f x₀) =O[𝓝[s] x₀] fun x => x - x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>x₀ : E<VAR>h : DifferentiableWithinAt 𝕜 f s x₀<GOAL>(fun x => f x - f x₀) =O[𝓝[s] x₀] fun x => x - x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x₀ : E<VAR>f' : E →L[𝕜] F<VAR>h : HasFDerivAt f f' x₀<GOAL>(fun x => f x - f x₀) =O[𝓝 x₀] fun x => x - x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x₀ : E<VAR>h : DifferentiableAt 𝕜 f x₀<GOAL>(fun x => f x - f x₀) =O[𝓝 x₀] fun x => x - x₀
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>hL : L ≤ 𝓝 x<VAR>h : HasFDerivAtFilter f f' x L<GOAL>Filter.Tendsto f L (𝓝 (f x))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<GOAL>ContinuousAt f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>h : DifferentiableAt 𝕜 f x<GOAL>ContinuousAt f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜 f s<GOAL>ContinuousOn f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>h : Differentiable 𝕜 f<GOAL>Continuous f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<GOAL>ContinuousAt f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>f' : E ≃L[𝕜] F<VAR>hf : HasStrictFDerivAt f (↑f') x<GOAL>(fun p => p.1 - p.2) =O[𝓝 (x, x)] fun p => f p.1 - f p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>C : ℝ≥0<VAR>hf' : AntilipschitzWith C ⇑f'<GOAL>(fun x' => x' - x) =O[L] fun x' => f x' - f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s t : Set E<VAR>h : s =ᶠ[𝓝 x] t<GOAL>HasFDerivWithinAt f f' s x ↔ HasFDerivWithinAt f f' t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>h : s =ᶠ[𝓝 x] t<GOAL>DifferentiableWithinAt 𝕜 f s x ↔ DifferentiableWithinAt 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>h : s =ᶠ[𝓝 x] t<GOAL>fderivWithin 𝕜 f s x = fderivWithin 𝕜 f t x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>y : E<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>fderivWithin 𝕜 f s =ᶠ[𝓝 x] fderivWithin 𝕜 f t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>x : E<VAR>s t : Set E<VAR>h : s =ᶠ[𝓝 x] t<GOAL>fderivWithin 𝕜 f s =ᶠ[𝓝 x] fderivWithin 𝕜 f t
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>f₀' f₁' : E →L[𝕜] F<VAR>x : E<VAR>h : f₀ =ᶠ[𝓝 x] f₁<VAR>h' : ∀ (y : E), f₀' y = f₁' y<GOAL>HasStrictFDerivAt f₀ f₀' x ↔ HasStrictFDerivAt f₁ f₁' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' g' : E →L[𝕜] F<VAR>x : E<VAR>h : HasStrictFDerivAt f f' x<VAR>h' : f' = g'<GOAL>HasStrictFDerivAt f g' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' g' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<VAR>h' : f' = g'<GOAL>HasFDerivAt f g' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : E → F<VAR>f' g' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>h : HasFDerivWithinAt f f' s x<VAR>h' : f' = g'<GOAL>HasFDerivWithinAt f g' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasStrictFDerivAt f f' x<VAR>h₁ : f =ᶠ[𝓝 x] f₁<GOAL>HasStrictFDerivAt f₁ f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>f₀' f₁' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>h₀ : f₀ =ᶠ[L] f₁<VAR>hx : f₀ x = f₁ x<VAR>h₁ : ∀ (x : E), f₀' x = f₁' x<GOAL>HasFDerivAtFilter f₀ f₀' x L ↔ HasFDerivAtFilter f₁ f₁' x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>h : HasFDerivAtFilter f f' x L<VAR>hL : f₁ =ᶠ[L] f<VAR>hx : f₁ x = f x<GOAL>HasFDerivAtFilter f₁ f' x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : f₀ =ᶠ[𝓝 x] f₁<GOAL>HasFDerivAt f₀ f' x ↔ HasFDerivAt f₁ f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f₀ f₁ : E → F<VAR>x : E<VAR>h : f₀ =ᶠ[𝓝 x] f₁<GOAL>DifferentiableAt 𝕜 f₀ x ↔ DifferentiableAt 𝕜 f₁ x