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>G : Type u_4<VAR>NormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>s : Set E<VAR>f₂ : E → F × G<VAR>h : DifferentiableOn 𝕜 f₂ s<GOAL>DifferentiableOn 𝕜 (fun x => (f₂ x).1) 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>p : E × F<GOAL>fderiv 𝕜 Prod.fst p = ContinuousLinearMap.fst 𝕜 E 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>x : E<VAR>f₂ : E → F × G<VAR>h : DifferentiableAt 𝕜 f₂ x<GOAL>fderiv 𝕜 (fun x => (f₂ x).1) x = (ContinuousLinearMap.fst 𝕜 F G).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>p : E × F<VAR>s : Set (E × F)<VAR>hs : UniqueDiffWithinAt 𝕜 s p<GOAL>fderivWithin 𝕜 Prod.fst s p = ContinuousLinearMap.fst 𝕜 E 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>x : E<VAR>s : Set E<VAR>f₂ : E → F × G<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableWithinAt 𝕜 f₂ s x<GOAL>fderivWithin 𝕜 (fun x => (f₂ x).1) s x = (ContinuousLinearMap.fst 𝕜 F G).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>p : E × F<GOAL>HasStrictFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p
<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>x : E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasStrictFDerivAt f₂ f₂' x<GOAL>HasStrictFDerivAt (fun x => (f₂ x).2) ((ContinuousLinearMap.snd 𝕜 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>p : E × F<VAR>L : Filter (E × F)<GOAL>HasFDerivAtFilter Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p 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>x : E<VAR>L : Filter E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasFDerivAtFilter f₂ f₂' x L<GOAL>HasFDerivAtFilter (fun x => (f₂ x).2) ((ContinuousLinearMap.snd 𝕜 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>p : E × F<GOAL>HasFDerivAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) p
<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>x : E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasFDerivAt f₂ f₂' x<GOAL>HasFDerivAt (fun x => (f₂ x).2) ((ContinuousLinearMap.snd 𝕜 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>p : E × F<VAR>s : Set (E × F)<GOAL>HasFDerivWithinAt Prod.snd (ContinuousLinearMap.snd 𝕜 E F) s p
<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>x : E<VAR>s : Set E<VAR>f₂ : E → F × G<VAR>f₂' : E →L[𝕜] F × G<VAR>h : HasFDerivWithinAt f₂ f₂' s x<GOAL>HasFDerivWithinAt (fun x => (f₂ x).2) ((ContinuousLinearMap.snd 𝕜 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>p : E × F<GOAL>DifferentiableAt 𝕜 Prod.snd p
<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>x : E<VAR>f₂ : E → F × G<VAR>h : DifferentiableAt 𝕜 f₂ x<GOAL>DifferentiableAt 𝕜 (fun x => (f₂ x).2) 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<GOAL>Differentiable 𝕜 Prod.snd
<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 × G<VAR>h : Differentiable 𝕜 f₂<GOAL>Differentiable 𝕜 fun x => (f₂ x).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>p : E × F<VAR>s : Set (E × F)<GOAL>DifferentiableWithinAt 𝕜 Prod.snd s p
<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>x : E<VAR>s : Set E<VAR>f₂ : E → F × G<VAR>h : DifferentiableWithinAt 𝕜 f₂ s x<GOAL>DifferentiableWithinAt 𝕜 (fun x => (f₂ x).2) 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>s : Set (E × F)<GOAL>DifferentiableOn 𝕜 Prod.snd 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>s : Set E<VAR>f₂ : E → F × G<VAR>h : DifferentiableOn 𝕜 f₂ s<GOAL>DifferentiableOn 𝕜 (fun x => (f₂ x).2) 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>p : E × F<GOAL>fderiv 𝕜 Prod.snd p = ContinuousLinearMap.snd 𝕜 E 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>x : E<VAR>f₂ : E → F × G<VAR>h : DifferentiableAt 𝕜 f₂ x<GOAL>fderiv 𝕜 (fun x => (f₂ x).2) x = (ContinuousLinearMap.snd 𝕜 F G).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>p : E × F<VAR>s : Set (E × F)<VAR>hs : UniqueDiffWithinAt 𝕜 s p<GOAL>fderivWithin 𝕜 Prod.snd s p = ContinuousLinearMap.snd 𝕜 E 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>x : E<VAR>s : Set E<VAR>f₂ : E → F × G<VAR>hs : UniqueDiffWithinAt 𝕜 s x<VAR>h : DifferentiableWithinAt 𝕜 f₂ s x<GOAL>fderivWithin 𝕜 (fun x => (f₂ x).2) s x = (ContinuousLinearMap.snd 𝕜 F G).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' : Type u_5<VAR>NormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>f₂ : G → G'<VAR>f₂' : G →L[𝕜] G'<VAR>p : E × G<VAR>hf : HasStrictFDerivAt f f' p.1<VAR>hf₂ : HasStrictFDerivAt f₂ f₂' p.2<GOAL>HasStrictFDerivAt (Prod.map f f₂) (f'.prodMap f₂') p
<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>f' : E →L[𝕜] F<VAR>f₂ : G → G'<VAR>f₂' : G →L[𝕜] G'<VAR>p : E × G<VAR>hf : HasFDerivAt f f' p.1<VAR>hf₂ : HasFDerivAt f₂ f₂' p.2<GOAL>HasFDerivAt (Prod.map f f₂) (f'.prodMap f₂') p
<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>f₂ : G → G'<VAR>p : E × G<VAR>hf : DifferentiableAt 𝕜 f p.1<VAR>hf₂ : DifferentiableAt 𝕜 f₂ p.2<GOAL>DifferentiableAt 𝕜 (fun p => (f p.1, f₂ p.2)) p
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>HasStrictFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasStrictFDerivAt (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>hφ : ∀ (i : ι), HasStrictFDerivAt (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x<GOAL>HasStrictFDerivAt Φ Φ' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>i : ι<VAR>f : (i : ι) → F' i<GOAL>HasStrictFDerivAt (fun f => f i) (ContinuousLinearMap.proj i) f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<GOAL>HasStrictFDerivAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasStrictFDerivAt (φ i) (φ' i) x
<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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>HasFDerivAtFilter Φ Φ' x L ↔ ∀ (i : ι), HasFDerivAtFilter (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x L
<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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<GOAL>HasFDerivAtFilter (fun x i => φ i x) (ContinuousLinearMap.pi φ') x L ↔ ∀ (i : ι), HasFDerivAtFilter (φ i) (φ' i) x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>HasFDerivAt Φ Φ' x ↔ ∀ (i : ι), HasFDerivAt (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>hφ : ∀ (i : ι), HasFDerivAt (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') x<GOAL>HasFDerivAt Φ Φ' x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>i : ι<VAR>f : (i : ι) → F' i<GOAL>HasFDerivAt (fun f => f i) (ContinuousLinearMap.proj i) f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<GOAL>HasFDerivAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') x ↔ ∀ (i : ι), HasFDerivAt (φ i) (φ' i) 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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<GOAL>HasFDerivWithinAt Φ Φ' s x ↔ ∀ (i : ι), HasFDerivWithinAt (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') s 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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>Φ' : E →L[𝕜] (i : ι) → F' i<VAR>hφ : ∀ (i : ι), HasFDerivWithinAt (fun x => Φ x i) ((ContinuousLinearMap.proj i).comp Φ') s x<GOAL>HasFDerivWithinAt Φ Φ' s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<GOAL>HasFDerivWithinAt (fun f => f i) (ContinuousLinearMap.proj i) s' f
<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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>φ' : (i : ι) → E →L[𝕜] F' i<GOAL>HasFDerivWithinAt (fun x i => φ i x) (ContinuousLinearMap.pi φ') s x ↔ ∀ (i : ι), HasFDerivWithinAt (φ i) (φ' i) s 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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>DifferentiableWithinAt 𝕜 Φ s x ↔ ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => Φ x i) s 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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>hφ : ∀ (i : ι), DifferentiableWithinAt 𝕜 (fun x => Φ x i) s x<GOAL>DifferentiableWithinAt 𝕜 Φ s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>i : ι<VAR>f : (i : ι) → F' i<VAR>s' : Set ((i : ι) → F' i)<GOAL>DifferentiableWithinAt 𝕜 (fun f => f i) s' f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>DifferentiableAt 𝕜 Φ x ↔ ∀ (i : ι), DifferentiableAt 𝕜 (fun x => Φ x i) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>hφ : ∀ (i : ι), DifferentiableAt 𝕜 (fun x => Φ x i) x<GOAL>DifferentiableAt 𝕜 Φ x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>i : ι<VAR>f : (i : ι) → F' i<GOAL>DifferentiableAt 𝕜 (fun f => f i) f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>DifferentiableOn 𝕜 Φ s ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => Φ x i) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>s : Set E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>hφ : ∀ (i : ι), DifferentiableOn 𝕜 (fun x => Φ x i) s<GOAL>DifferentiableOn 𝕜 Φ s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>i : ι<VAR>s' : Set ((i : ι) → F' i)<GOAL>DifferentiableOn 𝕜 (fun f => f i) s'
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<GOAL>Differentiable 𝕜 Φ ↔ ∀ (i : ι), Differentiable 𝕜 fun x => Φ x i
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>Φ : E → (i : ι) → F' i<VAR>hφ : ∀ (i : ι), Differentiable 𝕜 fun x => Φ x i<GOAL>Differentiable 𝕜 Φ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>i : ι<GOAL>Differentiable 𝕜 fun f => f i
<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>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>h : ∀ (i : ι), DifferentiableWithinAt 𝕜 (φ i) s x<VAR>hs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x i => φ i x) s x = ContinuousLinearMap.pi fun i => fderivWithin 𝕜 (φ i) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>ι : Type u_6<VAR>Fintype ι<VAR>F' : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (F' i)<VAR>(i : ι) → NormedSpace 𝕜 (F' i)<VAR>φ : (i : ι) → E → F' i<VAR>h : ∀ (i : ι), DifferentiableAt 𝕜 (φ i) x<GOAL>fderiv 𝕜 (fun x i => φ i x) x = ContinuousLinearMap.pi fun i => fderiv 𝕜 (φ i) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E → F<VAR>s : Set E<VAR>x : E<VAR>f' : E →L[ℝ] F<VAR>f_diff : DifferentiableOn ℝ f s<VAR>s_conv : Convex ℝ s<VAR>s_open : IsOpen s<VAR>f_cont : ∀ y ∈ closure s, ContinuousWithinAt f s y<VAR>h : Filter.Tendsto (fun y => fderiv ℝ f y) (𝓝[s] x) (𝓝 f')<GOAL>HasFDerivWithinAt f f' (closure s) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[>] a<VAR>f_lim' : Filter.Tendsto (fun x => deriv f x) (𝓝[>] a) (𝓝 e)<GOAL>HasDerivWithinAt f e (Set.Ici a) a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>s : Set ℝ<VAR>e : E<VAR>a : ℝ<VAR>f : ℝ → E<VAR>f_diff : DifferentiableOn ℝ f s<VAR>f_lim : ContinuousWithinAt f s a<VAR>hs : s ∈ 𝓝[<] a<VAR>f_lim' : Filter.Tendsto (fun x => deriv f x) (𝓝[<] a) (𝓝 e)<GOAL>HasDerivWithinAt f e (Set.Iic a) a
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : ℝ → E<VAR>x : ℝ<VAR>f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<GOAL>HasDerivAt f (g x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : ℝ → E<VAR>x : ℝ<VAR>f_diff : ∀ (y : ℝ), y ≠ x → HasDerivAt f (g y) y<VAR>hf : ContinuousAt f x<VAR>hg : ContinuousAt g x<VAR>y : ℝ<GOAL>HasDerivAt f (g y) y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<GOAL>iteratedDerivWithin n f Set.univ = iteratedDeriv n f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>iteratedDerivWithin n f s x = (iteratedFDerivWithin 𝕜 n f s x) fun x => 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<GOAL>iteratedDerivWithin n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F).symm ∘ iteratedFDerivWithin 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<GOAL>iteratedFDerivWithin 𝕜 n f s = ⇑(ContinuousMultilinearMap.piFieldEquiv 𝕜 (Fin n) F) ∘ iteratedDerivWithin n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>m : Fin n → 𝕜<GOAL>(iteratedFDerivWithin 𝕜 n f s x) m = (∏ i : Fin n, m i) • iteratedDerivWithin n f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>n : ℕ<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<GOAL>‖iteratedFDerivWithin 𝕜 n f s x‖ = ‖iteratedDerivWithin n f s x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<GOAL>iteratedDerivWithin 0 f s = f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>h : UniqueDiffWithinAt 𝕜 s x<GOAL>iteratedDerivWithin 1 f s x = derivWithin f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>n : ℕ∞<VAR>Hcont : ∀ (m : ℕ), ↑m ≤ n → ContinuousOn (fun x => iteratedDerivWithin m f s x) s<VAR>Hdiff : ∀ (m : ℕ), ↑m < n → DifferentiableOn 𝕜 (fun x => iteratedDerivWithin m f s x) s<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>n : ℕ∞<VAR>h : ∀ (m : ℕ), ↑m ≤ n → DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s<GOAL>ContDiffOn 𝕜 n f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>F : Type u_2<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<VAR>n : ℕ∞<VAR>m : ℕ<VAR>h : ContDiffOn 𝕜 n f s<VAR>hmn : ↑m ≤ n<VAR>hs : UniqueDiffOn 𝕜 s<GOAL>ContinuousOn (iteratedDerivWithin m f s) s