ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<GOAL>HasGradientWithinAt f f' s x ↔ (fun x' => f x' - f x - ⟪f', x' - x⟫_𝕜) =o[𝓝[s] x] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<GOAL>HasGradientWithinAt f f' s x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - ⟪f', x' - x⟫_𝕜‖) (𝓝[s] x) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<GOAL>HasGradientAt f f' x ↔ (fun x' => f x' - f x - ⟪f', x' - x⟫_𝕜) =o[𝓝 x] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<GOAL>HasGradientAt f f' x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - ⟪f', x' - x⟫_𝕜‖) (𝓝 x) (𝓝 0)
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>L : Filter F<VAR>h : HasGradientAtFilter f f' x L<GOAL>(fun x' => f x' - f x) =O[L] fun x' => x' - x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s t : Set F<VAR>y : F<VAR>h : s =ᶠ[𝓝[{y}ᶜ] x] t<GOAL>HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s t : Set F<VAR>h : s =ᶠ[𝓝 x] t<GOAL>HasGradientWithinAt f f' s x ↔ HasGradientWithinAt f f' t x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<GOAL>HasGradientAt f f' x ↔ (fun h => f (x + h) - f x - ⟪f', h⟫_𝕜) =o[𝓝 0] fun h => h
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>x : F<VAR>L : Filter F<VAR>f₀ f₁ : F → 𝕜<VAR>f₀' f₁' : F<VAR>h₀ : f₀ =ᶠ[L] f₁<VAR>hx : f₀ x = f₁ x<VAR>h₁ : f₀' = f₁'<GOAL>HasGradientAtFilter f₀ f₀' x L ↔ HasGradientAtFilter f₁ f₁' x L
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>L : Filter F<VAR>f₁ : F → 𝕜<VAR>h : HasGradientAtFilter f f' x L<VAR>hL : f₁ =ᶠ[L] f<VAR>hx : f₁ x = f x<GOAL>HasGradientAtFilter f₁ f' x L
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>f₁ : F → 𝕜<VAR>t : Set F<VAR>h : HasGradientWithinAt f f' s x<VAR>ht : ∀ x ∈ t, f₁ x = f x<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>HasGradientWithinAt f₁ f' t x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>f₁ : F → 𝕜<VAR>h : HasGradientWithinAt f f' s x<VAR>hs : ∀ x ∈ s, f₁ x = f x<VAR>hx : f₁ x = f x<GOAL>HasGradientWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>f₁ : F → 𝕜<VAR>h : HasGradientWithinAt f f' s x<VAR>hs : ∀ x ∈ s, f₁ x = f x<VAR>hx : x ∈ s<GOAL>HasGradientWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>f₁ : F → 𝕜<VAR>h : HasGradientWithinAt f f' s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasGradientWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>f₁ : F → 𝕜<VAR>h : HasGradientWithinAt f f' s x<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : x ∈ s<GOAL>HasGradientWithinAt f₁ f' s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>f₁ : F → 𝕜<VAR>h : HasGradientAt f f' x<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>HasGradientAt f₁ f' x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>f₁ : F → 𝕜<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>∇ f₁ x = ∇ f x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>x : F<VAR>f₁ : F → 𝕜<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>∇ f₁ =ᶠ[𝓝 x] ∇ f
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>x : F<VAR>L : Filter F<VAR>c : 𝕜<GOAL>HasGradientAtFilter (fun x => c) 0 x L
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>x : F<VAR>s : Set F<VAR>c : 𝕜<GOAL>HasGradientWithinAt (fun x => c) 0 s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>x : F<VAR>c : 𝕜<GOAL>HasGradientAt (fun x => c) 0 x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>x : F<VAR>c : 𝕜<GOAL>∇ (fun x => c) x = 0
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>c : 𝕜<GOAL>(∇ fun x => c) = fun x => 0
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>L : Filter F<VAR>hL : L ≤ 𝓝 x<VAR>h : HasGradientAtFilter f f' x L<GOAL>Filter.Tendsto f L (𝓝 (f x))
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>s : Set F<VAR>h : HasGradientWithinAt f f' s x<GOAL>ContinuousWithinAt f s x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>f' x : F<VAR>h : HasGradientAt f f' x<GOAL>ContinuousAt f x
<VAR>𝕜 : Type u_1<VAR>F : Type u_2<VAR>RCLike 𝕜<VAR>NormedAddCommGroup F<VAR>InnerProductSpace 𝕜 F<VAR>CompleteSpace F<VAR>f : F → 𝕜<VAR>s : Set F<VAR>f' : F → F<VAR>h : ∀ x ∈ s, HasGradientAt f (f' x) x<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>f' : E →L[𝕜] F<VAR>x : E<VAR>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : HasStrictFDerivAt f f' x<VAR>c : R<GOAL>HasStrictFDerivAt (fun x => c • f x) (c • 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>L : Filter E<VAR>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : HasFDerivAtFilter f f' x L<VAR>c : R<GOAL>HasFDerivAtFilter (fun x => c • f x) (c • 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 : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : HasFDerivWithinAt f f' s x<VAR>c : R<GOAL>HasFDerivWithinAt (fun x => c • f x) (c • 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>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : HasFDerivAt f f' x<VAR>c : R<GOAL>HasFDerivAt (fun x => c • f x) (c • 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>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>c : R<GOAL>DifferentiableWithinAt 𝕜 (fun y => c • f y) 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>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : DifferentiableAt 𝕜 f x<VAR>c : R<GOAL>DifferentiableAt 𝕜 (fun y => c • f y) 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>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : DifferentiableOn 𝕜 f s<VAR>c : R<GOAL>DifferentiableOn 𝕜 (fun y => c • f y) 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>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : Differentiable 𝕜 f<VAR>c : R<GOAL>Differentiable 𝕜 fun y => c • 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>x : E<VAR>s : Set E<VAR>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableWithinAt 𝕜 f s x<VAR>c : R<GOAL>fderivWithin 𝕜 (fun y => c • f y) s x = c • 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<VAR>x : E<VAR>R : Type u_6<VAR>Semiring R<VAR>Module R F<VAR>SMulCommClass 𝕜 R F<VAR>ContinuousConstSMul R F<VAR>h : DifferentiableAt 𝕜 f x<VAR>c : R<GOAL>fderiv 𝕜 (fun y => c • f y) x = c • 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 g : E → F<VAR>f' g' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<GOAL>HasStrictFDerivAt (fun y => f y + g y) (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 g : E → F<VAR>f' g' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hg : HasFDerivAtFilter g g' x L<GOAL>HasFDerivAtFilter (fun y => f y + g y) (f' + g') 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 g : E → F<VAR>f' g' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt g g' s x<GOAL>HasFDerivWithinAt (fun y => f y + g y) (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 g : E → F<VAR>f' g' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>hg : HasFDerivAt g g' x<GOAL>HasFDerivAt (fun x => f x + g x) (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 g : E → F<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hg : DifferentiableWithinAt 𝕜 g s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => f y + g y) 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 g : E → F<VAR>x : E<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>DifferentiableAt 𝕜 (fun y => f y + g y) 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 g : E → F<VAR>s : Set E<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hg : DifferentiableOn 𝕜 g s<GOAL>DifferentiableOn 𝕜 (fun y => f y + g y) 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 g : E → F<VAR>hf : Differentiable 𝕜 f<VAR>hg : Differentiable 𝕜 g<GOAL>Differentiable 𝕜 fun y => f y + g 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 g : E → F<VAR>x : E<VAR>s : Set E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hg : DifferentiableWithinAt 𝕜 g s x<GOAL>fderivWithin 𝕜 (fun y => f y + g y) s x = fderivWithin 𝕜 f s x + fderivWithin 𝕜 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 g : E → F<VAR>x : E<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>fderiv 𝕜 (fun y => f y + g y) x = fderiv 𝕜 f x + fderiv 𝕜 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' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<VAR>c : F<GOAL>HasStrictFDerivAt (fun y => f y + c) 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>L : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>c : F<GOAL>HasFDerivAtFilter (fun y => f y + c) 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 : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>c : F<GOAL>HasFDerivWithinAt (fun y => f y + c) 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 : HasFDerivAt f f' x<VAR>c : F<GOAL>HasFDerivAt (fun x => f x + c) 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>hf : DifferentiableWithinAt 𝕜 f s x<VAR>c : F<GOAL>DifferentiableWithinAt 𝕜 (fun y => f y + c) 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>c : F<GOAL>DifferentiableWithinAt 𝕜 (fun y => f y + c) s 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>hf : DifferentiableAt 𝕜 f x<VAR>c : F<GOAL>DifferentiableAt 𝕜 (fun y => f y + c) 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>c : F<GOAL>DifferentiableAt 𝕜 (fun y => f y + c) 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>s : Set E<VAR>hf : DifferentiableOn 𝕜 f s<VAR>c : F<GOAL>DifferentiableOn 𝕜 (fun y => f y + c) 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>c : F<GOAL>DifferentiableOn 𝕜 (fun y => f y + c) s ↔ 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>hf : Differentiable 𝕜 f<VAR>c : F<GOAL>Differentiable 𝕜 fun y => f y + 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>c : F<GOAL>(Differentiable 𝕜 fun y => f y + c) ↔ 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>x : E<VAR>s : Set E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>fderivWithin 𝕜 (fun y => f y + c) s 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<VAR>x : E<VAR>c : F<GOAL>fderiv 𝕜 (fun y => f y + c) 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>f' : E →L[𝕜] F<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<VAR>c : F<GOAL>HasStrictFDerivAt (fun y => c + f y) 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>L : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>c : F<GOAL>HasFDerivAtFilter (fun y => c + f y) 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 : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>c : F<GOAL>HasFDerivWithinAt (fun y => c + f y) 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 : HasFDerivAt f f' x<VAR>c : F<GOAL>HasFDerivAt (fun x => c + 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>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>c : F<GOAL>DifferentiableWithinAt 𝕜 (fun y => c + f y) 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>c : F<GOAL>DifferentiableWithinAt 𝕜 (fun y => c + f y) s 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>hf : DifferentiableAt 𝕜 f x<VAR>c : F<GOAL>DifferentiableAt 𝕜 (fun y => c + f y) 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>c : F<GOAL>DifferentiableAt 𝕜 (fun y => c + f y) 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>s : Set E<VAR>hf : DifferentiableOn 𝕜 f s<VAR>c : F<GOAL>DifferentiableOn 𝕜 (fun y => c + f y) 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>c : F<GOAL>DifferentiableOn 𝕜 (fun y => c + f y) s ↔ 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>hf : Differentiable 𝕜 f<VAR>c : F<GOAL>Differentiable 𝕜 fun y => c + 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>c : F<GOAL>(Differentiable 𝕜 fun y => c + f y) ↔ 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>x : E<VAR>s : Set E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>c : F<GOAL>fderivWithin 𝕜 (fun y => c + f y) s 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<VAR>x : E<VAR>c : F<GOAL>fderiv 𝕜 (fun y => c + f y) 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>x : E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, HasStrictFDerivAt (A i) (A' i) x<GOAL>HasStrictFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) 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>x : E<VAR>L : Filter E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, HasFDerivAtFilter (A i) (A' i) x L<GOAL>HasFDerivAtFilter (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) 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>x : E<VAR>s : Set E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, HasFDerivWithinAt (A i) (A' i) s x<GOAL>HasFDerivWithinAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) 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>x : E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>A' : ι → E →L[𝕜] F<VAR>h : ∀ i ∈ u, HasFDerivAt (A i) (A' i) x<GOAL>HasFDerivAt (fun y => ∑ i ∈ u, A i y) (∑ i ∈ u, A' i) 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>x : E<VAR>s : Set E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => ∑ i ∈ u, A i y) 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>x : E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x<GOAL>DifferentiableAt 𝕜 (fun y => ∑ i ∈ u, A i y) x