ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f f₁ : E → F<VAR>f' : F<VAR>x v : E<VAR>h : HasLineDerivAt 𝕜 f f' x v<VAR>h₁ : f₁ =ᶠ[𝓝 x] f<GOAL>HasLineDerivAt 𝕜 f₁ f' x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f s x v<VAR>h₁ : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>LineDifferentiableWithinAt 𝕜 f₁ s x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f f₁ : E → F<VAR>x v : E<VAR>h : LineDifferentiableAt 𝕜 f x v<VAR>hL : f₁ =ᶠ[𝓝 x] f<GOAL>LineDifferentiableAt 𝕜 f₁ x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>hs : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>lineDerivWithin 𝕜 f₁ s x v = lineDerivWithin 𝕜 f s x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f f₁ : E → F<VAR>x v : E<VAR>h : f₁ =ᶠ[𝓝 x] f<GOAL>lineDeriv 𝕜 f₁ x v = lineDeriv 𝕜 f x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : E<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>C : ℝ<VAR>hC₀ : 0 ≤ C<VAR>hlip : ∀ᶠ (x : E) in 𝓝 x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖<GOAL>‖f'‖ ≤ C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : E<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>s : Set E<VAR>hs : s ∈ 𝓝 x₀<VAR>C : ℝ≥0<VAR>hlip : LipschitzOnWith C f s<GOAL>‖f'‖ ≤ ↑C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : E<VAR>f : E → F<VAR>f' : F<VAR>x₀ : E<VAR>hf : HasLineDerivAt 𝕜 f f' x₀ v<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖f'‖ ≤ ↑C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : E<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>‖lineDeriv 𝕜 f x₀ v‖ ≤ C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : E<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>‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>v : E<VAR>f : E → F<VAR>x₀ : E<VAR>C : ℝ≥0<VAR>hlip : LipschitzWith C f<GOAL>‖lineDeriv 𝕜 f x₀ v‖ ≤ ↑C * ‖v‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>HasLineDerivWithinAt 𝕜 f 0 s x 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x : E<GOAL>HasLineDerivAt 𝕜 f 0 x 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x : E<GOAL>LineDifferentiableWithinAt 𝕜 f s x 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x : E<GOAL>LineDifferentiableAt 𝕜 f x 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x : E<GOAL>lineDeriv 𝕜 f x 0 = 0
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>E' : Type u_4<VAR>AddCommGroup E'<VAR>Module 𝕜 E'<VAR>f : E → F<VAR>f' : F<VAR>x : E'<VAR>L : E' →ₗ[𝕜] E<VAR>v : E'<VAR>hf : HasLineDerivAt 𝕜 (f ∘ ⇑L) f' x v<GOAL>HasLineDerivAt 𝕜 f f' (L x) (L v)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>E' : Type u_4<VAR>AddCommGroup E'<VAR>Module 𝕜 E'<VAR>f : E → F<VAR>x : E'<VAR>L : E' →ₗ[𝕜] E<VAR>v : E'<VAR>hf : LineDifferentiableAt 𝕜 (f ∘ ⇑L) x v<GOAL>LineDifferentiableAt 𝕜 f (L x) (L v)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>h : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>c : 𝕜<GOAL>HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>HasLineDerivWithinAt 𝕜 f (c • f') s x (c • v) ↔ HasLineDerivWithinAt 𝕜 f f' s x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x v : E<VAR>f' : F<VAR>h : HasLineDerivAt 𝕜 f f' x v<VAR>c : 𝕜<GOAL>HasLineDerivAt 𝕜 f (c • f') x (c • v)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x v : E<VAR>f' : F<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>HasLineDerivAt 𝕜 f (c • f') x (c • v) ↔ HasLineDerivAt 𝕜 f f' x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f s x v<VAR>c : 𝕜<GOAL>LineDifferentiableWithinAt 𝕜 f s x (c • v)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>LineDifferentiableWithinAt 𝕜 f s x (c • v) ↔ LineDifferentiableWithinAt 𝕜 f s x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x v : E<VAR>h : LineDifferentiableAt 𝕜 f x v<VAR>c : 𝕜<GOAL>LineDifferentiableAt 𝕜 f x (c • v)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x v : E<VAR>c : 𝕜<VAR>hc : c ≠ 0<GOAL>LineDifferentiableAt 𝕜 f x (c • v) ↔ LineDifferentiableAt 𝕜 f x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x v : E<VAR>c : 𝕜<GOAL>lineDeriv 𝕜 f x (c • v) = c • lineDeriv 𝕜 f x v
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>E : Type u_3<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x v : E<GOAL>lineDeriv 𝕜 f x (-v) = -lineDeriv 𝕜 f x 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>e : E →L[𝕜] F<VAR>x : E<GOAL>HasStrictFDerivAt (⇑e) e 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>e : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<GOAL>HasFDerivAtFilter (⇑e) e 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>e : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<GOAL>HasFDerivWithinAt (⇑e) e 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>e : E →L[𝕜] F<VAR>x : E<GOAL>HasFDerivAt (⇑e) e 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>e : E →L[𝕜] F<VAR>x : E<GOAL>DifferentiableAt 𝕜 (⇑e) 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>e : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<GOAL>DifferentiableWithinAt 𝕜 (⇑e) 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>e : E →L[𝕜] F<VAR>x : E<GOAL>fderiv 𝕜 (⇑e) x = e
<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>e : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (⇑e) s x = e
<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>e : E →L[𝕜] F<GOAL>Differentiable 𝕜 ⇑e
<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>e : E →L[𝕜] F<VAR>s : Set E<GOAL>DifferentiableOn 𝕜 (⇑e) 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>L : Filter E<VAR>h : IsBoundedLinearMap 𝕜 f<GOAL>HasFDerivAtFilter f h.toContinuousLinearMap 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>x : E<VAR>s : Set E<VAR>h : IsBoundedLinearMap 𝕜 f<GOAL>HasFDerivWithinAt f h.toContinuousLinearMap 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 : IsBoundedLinearMap 𝕜 f<GOAL>HasFDerivAt f h.toContinuousLinearMap 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 : IsBoundedLinearMap 𝕜 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 : IsBoundedLinearMap 𝕜 f<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 : IsBoundedLinearMap 𝕜 f<GOAL>fderiv 𝕜 f x = h.toContinuousLinearMap
<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 : IsBoundedLinearMap 𝕜 f<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 f s x = h.toContinuousLinearMap
<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 : IsBoundedLinearMap 𝕜 f<GOAL>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 : IsBoundedLinearMap 𝕜 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>g : F → G<VAR>g' : F →L[𝕜] G<VAR>L' : Filter F<VAR>hg : HasFDerivAtFilter g g' (f x) L'<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hL : Filter.Tendsto f L L'<GOAL>HasFDerivAtFilter (g ∘ f) (g'.comp 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>g' : F →L[𝕜] G<VAR>t : Set F<VAR>hg : HasFDerivWithinAt g g' t (f x)<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hst : Set.MapsTo f s t<GOAL>HasFDerivWithinAt (g ∘ f) (g'.comp 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>g' : F →L[𝕜] G<VAR>hg : HasFDerivAt g g' (f x)<VAR>hf : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (g ∘ f) (g'.comp 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>g' : F →L[𝕜] G<VAR>t : Set F<VAR>hg : HasFDerivWithinAt g g' t (f x)<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hst : Filter.Tendsto f (𝓝[s] x) (𝓝[t] f x)<GOAL>HasFDerivWithinAt (g ∘ f) (g'.comp 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>g : F → G<VAR>g' : F →L[𝕜] G<VAR>hg : HasFDerivAt g g' (f x)<VAR>hf : HasFDerivAt f f' x<GOAL>HasFDerivAt (g ∘ f) (g'.comp 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>t : Set F<VAR>hg : DifferentiableWithinAt 𝕜 g t (f x)<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>h : Set.MapsTo f s t<GOAL>DifferentiableWithinAt 𝕜 (g ∘ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>t : Set F<VAR>hg : DifferentiableWithinAt 𝕜 g t (f x)<VAR>hf : DifferentiableWithinAt 𝕜 f s x<GOAL>DifferentiableWithinAt 𝕜 (g ∘ f) (s ∩ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>g : F → G<VAR>hg : DifferentiableAt 𝕜 g (f x)<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (g ∘ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>hg : DifferentiableAt 𝕜 g (f x)<VAR>hf : DifferentiableWithinAt 𝕜 f s x<GOAL>DifferentiableWithinAt 𝕜 (g ∘ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>t : Set F<VAR>hg : DifferentiableWithinAt 𝕜 g t (f x)<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>h : Set.MapsTo f s t<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>g : F → G<VAR>f : E → F<VAR>x : E<VAR>y : F<VAR>s : Set E<VAR>t : Set F<VAR>hg : DifferentiableWithinAt 𝕜 g t y<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>h : Set.MapsTo f s t<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>hy : f x = y<VAR>v : E<GOAL>(fderivWithin 𝕜 g t y) ((fderivWithin 𝕜 f s x) v) = (fderivWithin 𝕜 (g ∘ f) s x) 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>G' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>g' : G → G'<VAR>g : F → G<VAR>t : Set F<VAR>u : Set G<VAR>y : F<VAR>y' : G<VAR>hg' : DifferentiableWithinAt 𝕜 g' u y'<VAR>hg : DifferentiableWithinAt 𝕜 g t y<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>h2g : Set.MapsTo g t u<VAR>h2f : Set.MapsTo f s t<VAR>h3g : g y = y'<VAR>h3f : f x = y<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (g' ∘ g ∘ f) s x = (fderivWithin 𝕜 g' u y').comp ((fderivWithin 𝕜 g t y).comp (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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>g : F → G<VAR>hg : DifferentiableAt 𝕜 g (f x)<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>fderiv 𝕜 (g ∘ f) x = (fderiv 𝕜 g (f x)).comp (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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>g : F → G<VAR>hg : DifferentiableAt 𝕜 g (f x)<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (g ∘ f) s x = (fderiv 𝕜 g (f x)).comp (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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>s : Set E<VAR>g : F → G<VAR>t : Set F<VAR>hg : DifferentiableOn 𝕜 g t<VAR>hf : DifferentiableOn 𝕜 f s<VAR>st : Set.MapsTo f s t<GOAL>DifferentiableOn 𝕜 (g ∘ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>g : F → G<VAR>hg : Differentiable 𝕜 g<VAR>hf : Differentiable 𝕜 f<GOAL>Differentiable 𝕜 (g ∘ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>s : Set E<VAR>g : F → G<VAR>hg : Differentiable 𝕜 g<VAR>hf : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (g ∘ 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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>g : F → G<VAR>g' : F →L[𝕜] G<VAR>hg : HasStrictFDerivAt g g' (f x)<VAR>hf : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => g (f x)) (g'.comp f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → E<VAR>hf : Differentiable 𝕜 f<VAR>n : ℕ<GOAL>Differentiable 𝕜 f^[n]
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>f : E → E<VAR>hf : DifferentiableOn 𝕜 f s<VAR>hs : Set.MapsTo f s s<VAR>n : ℕ<GOAL>DifferentiableOn 𝕜 f^[n] s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>L : Filter E<VAR>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>hL : Filter.Tendsto f L L<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasFDerivAtFilter f^[n] (f' ^ n) x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasFDerivAt f^[n] (f' ^ n) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hx : f x = x<VAR>hs : Set.MapsTo f s s<VAR>n : ℕ<GOAL>HasFDerivWithinAt f^[n] (f' ^ n) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>f : E → E<VAR>f' : E →L[𝕜] E<VAR>hf : HasStrictFDerivAt f f' x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>HasStrictFDerivAt f^[n] (f' ^ n) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>f : E → E<VAR>hf : DifferentiableAt 𝕜 f x<VAR>hx : f x = x<VAR>n : ℕ<GOAL>DifferentiableAt 𝕜 f^[n] x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>s : Set E<VAR>f : E → E<VAR>hf : DifferentiableWithinAt 𝕜 f s x<VAR>hx : f x = x<VAR>hs : Set.MapsTo f s s<VAR>n : ℕ<GOAL>DifferentiableWithinAt 𝕜 f^[n] s x
<VAR>α : Type u_1<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>RCLike 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>CompleteSpace F<VAR>u : α → ℝ<VAR>NormedSpace 𝕜 F<VAR>f : α → E → F<VAR>f' : α → E → E →L[𝕜] F<VAR>s : Set E<VAR>x₀ x : E<VAR>hu : Summable u<VAR>hs : IsOpen s<VAR>h's : IsPreconnected s<VAR>hf : ∀ (n : α), ∀ x ∈ s, HasFDerivAt (f n) (f' n x) x<VAR>hf' : ∀ (n : α), ∀ x ∈ s, ‖f' n x‖ ≤ u n<VAR>hx₀ : x₀ ∈ s<VAR>hf0 : Summable fun x => f x x₀<VAR>hx : x ∈ s<GOAL>Summable fun n => f n x