ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ<VAR>hp : (↑(FiniteDimensional.finrank ℝ E)).IsConjExponent p<GOAL>∫⁻ (x : E), ↑‖u x‖₊ ^ p ∂μ ≤ ↑(MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p) * (∫⁻ (x : E), ↑‖fderiv ℝ u x‖₊ ∂μ) ^ p
<VAR>E : Type u_5<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>p : ℝ<GOAL>MeasureTheory.eLpNormLESNormFDerivOneConst μ p = MeasureTheory.lintegralPowLePowLIntegralFDerivConst μ p ^ p⁻¹
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p : ℝ≥0<VAR>hp : (↑(FiniteDimensional.finrank ℝ E)).IsConjExponent p<GOAL>MeasureTheory.eLpNorm u (↑p) μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOneConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) 1 μ
<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>F' : Type u_5<VAR>NormedAddCommGroup F'<VAR>InnerProductSpace ℝ F'<VAR>CompleteSpace F'<VAR>u : E → F'<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p p' : ℝ≥0<VAR>hp : 1 ≤ p<VAR>hn : 0 < FiniteDimensional.finrank ℝ E<VAR>hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(FiniteDimensional.finrank ℝ E))⁻¹<GOAL>MeasureTheory.eLpNorm u (↑p') μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>p : ℝ<GOAL>MeasureTheory.SNormLESNormFDerivOfEqConst F μ p = let F' := EuclideanSpace ℝ (Fin (FiniteDimensional.finrank ℝ F)); let e := toEuclidean; ‖↑e.symm‖₊ * MeasureTheory.eLpNormLESNormFDerivOfEqInnerConst μ p * ‖↑e‖₊
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>u : E → F<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : HasCompactSupport u<VAR>p p' : ℝ≥0<VAR>hp : 1 ≤ p<VAR>hn : 0 < FiniteDimensional.finrank ℝ E<VAR>hp' : (↑p')⁻¹ = ↑p⁻¹ - (↑(FiniteDimensional.finrank ℝ E))⁻¹<GOAL>MeasureTheory.eLpNorm u (↑p') μ ≤ ↑(MeasureTheory.SNormLESNormFDerivOfEqConst F μ ↑p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>F : Type u_6<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>E : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>s : Set E<VAR>p q : ℝ≥0<GOAL>MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p q = let p' := (p⁻¹ - (↑(FiniteDimensional.finrank ℝ E))⁻¹)⁻¹; (μ s).toNNReal ^ (1 / ↑q - 1 / ↑p') * MeasureTheory.SNormLESNormFDerivOfEqConst F μ ↑p
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>u : E → F<VAR>s : Set E<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : Function.support u ⊆ s<VAR>p q : ℝ≥0<VAR>hp : 1 ≤ p<VAR>h2p : p < ↑(FiniteDimensional.finrank ℝ E)<VAR>hpq : ↑p⁻¹ - (↑(FiniteDimensional.finrank ℝ E))⁻¹ ≤ (↑q)⁻¹<VAR>hs : Bornology.IsBounded s<GOAL>MeasureTheory.eLpNorm u (↑q) μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p q) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>FiniteDimensional ℝ E<VAR>μ : MeasureTheory.Measure E<VAR>μ.IsAddHaarMeasure<VAR>FiniteDimensional ℝ F<VAR>u : E → F<VAR>s : Set E<VAR>hu : ContDiff ℝ 1 u<VAR>h2u : Function.support u ⊆ s<VAR>p : ℝ≥0<VAR>hp : 1 ≤ p<VAR>h2p : p < ↑(FiniteDimensional.finrank ℝ E)<VAR>hs : Bornology.IsBounded s<GOAL>MeasureTheory.eLpNorm u (↑p) μ ≤ ↑(MeasureTheory.eLpNormLESNormFDerivOfLeConst F μ s p p) * MeasureTheory.eLpNorm (fderiv ℝ u) (↑p) μ
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasStrictFDerivAt f f' x<GOAL>HasStrictFDerivAt (fun x => star (f x)) ((↑(starL' 𝕜)).comp f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar 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 => star (f x)) ((↑(starL' 𝕜)).comp f') x L
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar 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 => star (f x)) ((↑(starL' 𝕜)).comp f') s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>f' : E →L[𝕜] F<VAR>x : E<VAR>h : HasFDerivAt f f' x<GOAL>HasFDerivAt (fun x => star (f x)) ((↑(starL' 𝕜)).comp f') x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>h : DifferentiableWithinAt 𝕜 f s x<GOAL>DifferentiableWithinAt 𝕜 (fun y => star (f y)) s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<GOAL>DifferentiableWithinAt 𝕜 (fun y => star (f y)) s x ↔ DifferentiableWithinAt 𝕜 f s x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>x : E<VAR>h : DifferentiableAt 𝕜 f x<GOAL>DifferentiableAt 𝕜 (fun y => star (f y)) x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>x : E<GOAL>DifferentiableAt 𝕜 (fun y => star (f y)) x ↔ DifferentiableAt 𝕜 f x
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>s : Set E<VAR>h : DifferentiableOn 𝕜 f s<GOAL>DifferentiableOn 𝕜 (fun y => star (f y)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>s : Set E<GOAL>DifferentiableOn 𝕜 (fun y => star (f y)) s ↔ DifferentiableOn 𝕜 f s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>h : Differentiable 𝕜 f<GOAL>Differentiable 𝕜 fun y => star (f y)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<GOAL>(Differentiable 𝕜 fun y => star (f y)) ↔ Differentiable 𝕜 f
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>x : E<VAR>s : Set E<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun y => star (f y)) s x = (↑(starL' 𝕜)).comp (fderivWithin 𝕜 f s x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>StarAddMonoid F<VAR>NormedSpace 𝕜 F<VAR>StarModule 𝕜 F<VAR>ContinuousStar F<VAR>f : E → F<VAR>x : E<GOAL>fderiv 𝕜 (fun y => star (f y)) x = (↑(starL' 𝕜)).comp (fderiv 𝕜 f x)
<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>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>hf : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>hst : t ⊆ s<GOAL>HasLineDerivWithinAt 𝕜 f f' t 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>f' : F<VAR>x v : E<VAR>hf : HasLineDerivAt 𝕜 f f' x v<VAR>s : Set E<GOAL>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>f' : F<VAR>s : Set E<VAR>x v : E<VAR>hf : HasLineDerivWithinAt 𝕜 f f' s x v<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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>f' : F<VAR>x v : E<VAR>hf : HasLineDerivAt 𝕜 f f' x v<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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f s x v<GOAL>HasLineDerivWithinAt 𝕜 f (lineDerivWithin 𝕜 f s x v) 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<GOAL>HasLineDerivAt 𝕜 f (lineDeriv 𝕜 f x v) 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>f' : F<VAR>x v : E<GOAL>HasLineDerivWithinAt 𝕜 f f' Set.univ x 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<GOAL>lineDerivWithin 𝕜 f s x v = 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 v : E<VAR>h : ¬LineDifferentiableAt 𝕜 f x v<GOAL>lineDeriv 𝕜 f x v = 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>f' : F<VAR>x v : E<GOAL>HasLineDerivAt 𝕜 f f' x v ↔ (fun t => f (x + t • v) - f x - t • f') =o[𝓝 0] fun t => t
<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>f₀' f₁' : F<VAR>x v : E<VAR>h₀ : HasLineDerivAt 𝕜 f f₀' x v<VAR>h₁ : HasLineDerivAt 𝕜 f f₁' x v<GOAL>f₀' = f₁'
<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>f' : F<VAR>x v : E<VAR>h : HasLineDerivAt 𝕜 f f' x v<GOAL>lineDeriv 𝕜 f x v = f'
<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>LineDifferentiableWithinAt 𝕜 f Set.univ x 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>s : Set E<VAR>x v : E<VAR>h : LineDifferentiableAt 𝕜 f x v<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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>x v : E<GOAL>lineDerivWithin 𝕜 f Set.univ 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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>s t : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f t x v<VAR>st : s ⊆ t<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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f f₁ : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>h : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>ht : Set.EqOn f₁ f t<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>HasLineDerivWithinAt 𝕜 f₁ f' t 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 f₁ : E → F<VAR>f' : F<VAR>s : Set E<VAR>x v : E<VAR>h : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>hs : Set.EqOn f₁ f s<VAR>hx : f₁ x = f x<GOAL>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 f₁ : E → F<VAR>f' : F<VAR>s : Set E<VAR>x v : E<VAR>h : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>hs : Set.EqOn f₁ f s<VAR>hx : x ∈ s<GOAL>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 f₁ : E → F<VAR>s t : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f s x v<VAR>ht : Set.EqOn f₁ f t<VAR>hx : f₁ x = f x<VAR>h₁ : t ⊆ s<GOAL>LineDifferentiableWithinAt 𝕜 f₁ t 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 f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f s x v<VAR>ht : ∀ x ∈ s, f₁ x = f x<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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>hs : Set.EqOn f₁ f s<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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>hs : Set.EqOn f₁ f s<VAR>hx : x ∈ s<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>AddCommGroup E<VAR>Module 𝕜 E<VAR>f : E → F<VAR>f' : F<VAR>x v : E<GOAL>HasLineDerivAt 𝕜 f f' x v ↔ Filter.Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (𝓝[≠] 0) (𝓝 f')
<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>f' : F<VAR>x v : E<VAR>PartialOrder 𝕜<VAR>h : HasLineDerivAt 𝕜 f f' x v<GOAL>Filter.Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (𝓝[>] 0) (𝓝 f')
<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>f' : F<VAR>x v : E<VAR>PartialOrder 𝕜<VAR>h : HasLineDerivAt 𝕜 f f' x v<GOAL>Filter.Tendsto (fun t => t⁻¹ • (f (x + t • v) - f x)) (𝓝[<] 0) (𝓝 f')
<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>f' : F<VAR>s : Set E<VAR>x v : E<VAR>h : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>hs : ∀ᶠ (t : 𝕜) in 𝓝 0, x + t • v ∈ s<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 : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>h : HasLineDerivWithinAt 𝕜 f f' t x v<VAR>hst : t ∈ 𝓝[s] x<GOAL>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>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f : E → F<VAR>f' : F<VAR>s : Set E<VAR>x v : E<VAR>h : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>hs : s ∈ 𝓝 x<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 : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f s x v<VAR>hs : s ∈ 𝓝 x<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 : E → F<VAR>s : Set E<VAR>x : E<VAR>L : E →L[𝕜] F<VAR>hf : HasFDerivWithinAt f L s x<VAR>v : E<GOAL>HasLineDerivWithinAt 𝕜 f (L v) 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 : E → F<VAR>x : E<VAR>L : E →L[𝕜] F<VAR>hf : HasFDerivAt f L x<VAR>v : E<GOAL>HasLineDerivAt 𝕜 f (L v) 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 : E → F<VAR>x v : E<VAR>hf : DifferentiableAt 𝕜 f x<GOAL>lineDeriv 𝕜 f x v = (fderiv 𝕜 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 : E → F<VAR>s t : Set E<VAR>x v : E<VAR>h : LineDifferentiableWithinAt 𝕜 f s x v<VAR>hst : s ∈ 𝓝[t] x<GOAL>LineDifferentiableWithinAt 𝕜 f t 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 : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : s ∈ 𝓝 x<GOAL>lineDerivWithin 𝕜 f s 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>f : E → F<VAR>s : Set E<VAR>x v : E<VAR>hs : IsOpen s<VAR>hx : x ∈ s<GOAL>lineDerivWithin 𝕜 f s 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>f : E → F<VAR>f' : F<VAR>s t : Set E<VAR>x v : E<VAR>h : s =ᶠ[𝓝 x] t<GOAL>HasLineDerivWithinAt 𝕜 f f' s x v ↔ HasLineDerivWithinAt 𝕜 f f' t 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 : E → F<VAR>s t : Set E<VAR>x v : E<VAR>h : s =ᶠ[𝓝 x] t<GOAL>LineDifferentiableWithinAt 𝕜 f s x v ↔ LineDifferentiableWithinAt 𝕜 f t 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 : E → F<VAR>s t : Set E<VAR>x v : E<VAR>h : s =ᶠ[𝓝 x] t<GOAL>lineDerivWithin 𝕜 f s x v = lineDerivWithin 𝕜 f t 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>f' : F<VAR>x v : E<VAR>h : f₀ =ᶠ[𝓝 x] f₁<GOAL>HasLineDerivAt 𝕜 f₀ f' x 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>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f₀ f₁ : E → F<VAR>x v : E<VAR>h : f₀ =ᶠ[𝓝 x] f₁<GOAL>LineDifferentiableAt 𝕜 f₀ x 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>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f₀ f₁ : E → F<VAR>f' : F<VAR>s : Set E<VAR>x v : E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : f₀ x = f₁ x<GOAL>HasLineDerivWithinAt 𝕜 f₀ f' s x 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>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f₀ f₁ : E → F<VAR>f' : F<VAR>s : Set E<VAR>x v : E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : x ∈ s<GOAL>HasLineDerivWithinAt 𝕜 f₀ f' s x 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>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f₀ f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : f₀ x = f₁ x<GOAL>LineDifferentiableWithinAt 𝕜 f₀ s x 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>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f₀ f₁ : E → F<VAR>s : Set E<VAR>x v : E<VAR>h : f₀ =ᶠ[𝓝[s] x] f₁<VAR>hx : x ∈ s<GOAL>LineDifferentiableWithinAt 𝕜 f₀ s x 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>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>f f₁ : E → F<VAR>f' : F<VAR>s : Set E<VAR>x v : E<VAR>hf : HasLineDerivWithinAt 𝕜 f f' s x v<VAR>h'f : f₁ =ᶠ[𝓝[s] x] f<VAR>hx : f₁ x = f x<GOAL>HasLineDerivWithinAt 𝕜 f₁ f' s x v