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>s : Set E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>h : ∀ i ∈ u, DifferentiableOn 𝕜 (A i) s<GOAL>DifferentiableOn 𝕜 (fun y => ∑ i ∈ u, A i 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>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>h : ∀ i ∈ u, Differentiable 𝕜 (A i)<GOAL>Differentiable 𝕜 fun y => ∑ i ∈ u, A i 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>x : E<VAR>s : Set E<VAR>ι : Type u_6<VAR>u : Finset ι<VAR>A : ι → E → F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<VAR>h : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (A i) s x<GOAL>fderivWithin 𝕜 (fun y => ∑ i ∈ u, A i y) s x = ∑ i ∈ u, fderivWithin 𝕜 (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>h : ∀ i ∈ u, DifferentiableAt 𝕜 (A i) x<GOAL>fderiv 𝕜 (fun y => ∑ i ∈ u, A i y) x = ∑ i ∈ u, fderiv 𝕜 (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>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (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>L : Filter E<VAR>h : HasFDerivAtFilter f f' x L<GOAL>HasFDerivAtFilter (fun x => -f x) (-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>h : HasFDerivWithinAt f f' s x<GOAL>HasFDerivWithinAt (fun x => -f x) (-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>HasFDerivAt (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>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => -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<GOAL>DifferentiableWithinAt 𝕜 (fun y => -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>h : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun y => -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<GOAL>DifferentiableAt 𝕜 (fun y => -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>h : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun y => -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<GOAL>DifferentiableOn 𝕜 (fun y => -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>h : Differentiable 𝕜 f<GOAL>Differentiable 𝕜 fun y => -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<GOAL>(Differentiable 𝕜 fun y => -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<GOAL>fderivWithin 𝕜 (fun y => -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<GOAL>fderiv 𝕜 (fun y => -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>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 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>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 x => f x - g x) (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 x => f x - g x) (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>x : E<VAR>hg : DifferentiableAt 𝕜 g x<GOAL>DifferentiableAt 𝕜 (fun y => f y + g 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 g : E → F<VAR>x : E<VAR>hg : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun y => f y + g y) x ↔ DifferentiableAt 𝕜 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>hg : DifferentiableAt 𝕜 g x<GOAL>DifferentiableAt 𝕜 (fun y => f y - g 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 g : E → F<VAR>x : E<VAR>hg : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 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>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>s : Set E<VAR>hg : DifferentiableOn 𝕜 g s<GOAL>DifferentiableOn 𝕜 (fun y => f y + g 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 g : E → F<VAR>s : Set E<VAR>hg : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun y => f y + g y) s ↔ DifferentiableOn 𝕜 g 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>s : Set E<VAR>hg : DifferentiableOn 𝕜 g s<GOAL>DifferentiableOn 𝕜 (fun y => f y - g 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 g : E → F<VAR>s : Set E<VAR>hg : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun y => f y - g y) s ↔ DifferentiableOn 𝕜 g 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>hg : Differentiable 𝕜 g<GOAL>(Differentiable 𝕜 fun y => f y + g 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 g : E → F<VAR>hg : Differentiable 𝕜 f<GOAL>(Differentiable 𝕜 fun y => f y + g y) ↔ Differentiable 𝕜 g
<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>hg : Differentiable 𝕜 g<GOAL>(Differentiable 𝕜 fun y => f y - g 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 g : E → F<VAR>hg : Differentiable 𝕜 f<GOAL>(Differentiable 𝕜 fun y => f y - g y) ↔ Differentiable 𝕜 g
<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 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>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>c : F<GOAL>HasFDerivAtFilter (fun x => 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>hf : HasFDerivWithinAt f f' s x<VAR>c : F<GOAL>HasFDerivWithinAt (fun x => 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>hf : HasFDerivAt f f' x<VAR>c : F<GOAL>HasFDerivAt (fun x => f x - c) f' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : F<VAR>c : F<GOAL>HasStrictFDerivAt (fun x => x - c) (ContinuousLinearMap.id 𝕜 F) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>x : F<VAR>c : F<GOAL>HasFDerivAt (fun x => x - c) (ContinuousLinearMap.id 𝕜 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 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>f' : E →L[𝕜] F<VAR>x : E<VAR>L : Filter E<VAR>hf : HasFDerivAtFilter f f' x L<VAR>c : F<GOAL>HasFDerivAtFilter (fun x => c - f x) (-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 x => c - f x) (-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 v<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>AddCommGroup E<VAR>Module 𝕜 E<VAR>TopologicalSpace E<VAR>TopologicalAddGroup E<VAR>ContinuousSMul 𝕜 E<VAR>T2Space E<VAR>FiniteDimensional 𝕜 E<VAR>CompleteSpace 𝕜<VAR>TietzeExtension 𝕜<GOAL>TietzeExtension E
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>TietzeExtension ↑(Metric.ball 0 r)
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>y : E<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>TietzeExtension ↑(Metric.closedBall y r)
<VAR>X : Type u<VAR>TopologicalSpace X<VAR>NormalSpace X<VAR>s : Set X<VAR>hs : IsClosed s<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>FiniteDimensional 𝕜 E<VAR>f : BoundedContinuousFunction (↑s) E<GOAL>∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f
<GOAL>Smooth 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) UpperHalfPlane.coe
<GOAL>MDifferentiable 𝓘(ℂ, ℂ) 𝓘(ℂ, ℂ) UpperHalfPlane.coe
<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>iso : E ≃L[𝕜] F<GOAL>HasStrictFDerivAt (⇑iso) (↑iso) 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>iso : E ≃L[𝕜] F<GOAL>HasFDerivWithinAt (⇑iso) (↑iso) 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>iso : E ≃L[𝕜] F<GOAL>HasFDerivAt (⇑iso) (↑iso) 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>iso : E ≃L[𝕜] F<GOAL>DifferentiableAt 𝕜 (⇑iso) 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>iso : E ≃L[𝕜] F<GOAL>DifferentiableWithinAt 𝕜 (⇑iso) 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>iso : E ≃L[𝕜] F<GOAL>fderiv 𝕜 (⇑iso) x = ↑iso
<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>iso : E ≃L[𝕜] F<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (⇑iso) s x = ↑iso
<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>iso : E ≃L[𝕜] F<GOAL>Differentiable 𝕜 ⇑iso
<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>s : Set E<VAR>iso : E ≃L[𝕜] F<GOAL>DifferentiableOn 𝕜 (⇑iso) s