ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>x_ne_zero : x ≠ 0<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt (fun x => x⁻¹) (-(x ^ 2)⁻¹) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>DifferentiableAt 𝕜 (fun x => x⁻¹) x ↔ x ≠ 0
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>x_ne_zero : x ≠ 0<GOAL>DifferentiableWithinAt 𝕜 (fun x => x⁻¹) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<GOAL>DifferentiableOn 𝕜 (fun x => x⁻¹) {x | x ≠ 0}
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>deriv (fun x => x⁻¹) x = -(x ^ 2)⁻¹
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<GOAL>(deriv fun x => x⁻¹) = fun x => -(x ^ 2)⁻¹
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>x_ne_zero : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => x⁻¹) s x = -(x ^ 2)⁻¹
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>x_ne_zero : x ≠ 0<GOAL>HasFDerivAt (fun x => x⁻¹) (ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>x_ne_zero : x ≠ 0<GOAL>HasFDerivWithinAt (fun x => x⁻¹) (ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<GOAL>fderiv 𝕜 (fun x => x⁻¹) x = ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>x_ne_zero : x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>fderivWithin 𝕜 (fun x => x⁻¹) s x = ContinuousLinearMap.smulRight 1 (-(x ^ 2)⁻¹)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>hc : HasDerivWithinAt c c' s x<VAR>hx : c x ≠ 0<GOAL>HasDerivWithinAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>c : 𝕜 → 𝕜<VAR>c' : 𝕜<VAR>hc : HasDerivAt c c' x<VAR>hx : c x ≠ 0<GOAL>HasDerivAt (fun y => (c y)⁻¹) (-c' / c x ^ 2) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>h : E → 𝕜<VAR>z : E<VAR>S : Set E<VAR>hf : DifferentiableWithinAt 𝕜 h S z<VAR>hz : h z ≠ 0<GOAL>DifferentiableWithinAt 𝕜 (fun x => (h x)⁻¹) S z
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>h : E → 𝕜<VAR>z : E<VAR>hf : DifferentiableAt 𝕜 h z<VAR>hz : h z ≠ 0<GOAL>DifferentiableAt 𝕜 (fun x => (h x)⁻¹) z
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>h : E → 𝕜<VAR>S : Set E<VAR>hf : DifferentiableOn 𝕜 h S<VAR>hz : ∀ x ∈ S, h x ≠ 0<GOAL>DifferentiableOn 𝕜 (fun x => (h x)⁻¹) S
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>E : Type w<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>h : E → 𝕜<VAR>hf : Differentiable 𝕜 h<VAR>hz : ∀ (x : E), h x ≠ 0<GOAL>Differentiable 𝕜 fun x => (h x)⁻¹
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>c : 𝕜 → 𝕜<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hx : c x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => (c x)⁻¹) s x = -derivWithin c s x / c x ^ 2
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>c : 𝕜 → 𝕜<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hx : c x ≠ 0<GOAL>deriv (fun x => (c x)⁻¹) x = -deriv c x / c x ^ 2
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivWithinAt c c' s x<VAR>hd : HasDerivWithinAt d d' s x<VAR>hx : d x ≠ 0<GOAL>HasDerivWithinAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasStrictDerivAt c c' x<VAR>hd : HasStrictDerivAt d d' x<VAR>hx : d x ≠ 0<GOAL>HasStrictDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>c' d' : 𝕜'<VAR>hc : HasDerivAt c c' x<VAR>hd : HasDerivAt d d' x<VAR>hx : d x ≠ 0<GOAL>HasDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hd : DifferentiableWithinAt 𝕜 d s x<VAR>hx : d x ≠ 0<GOAL>DifferentiableWithinAt 𝕜 (fun x => c x / d x) s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hd : DifferentiableAt 𝕜 d x<VAR>hx : d x ≠ 0<GOAL>DifferentiableAt 𝕜 (fun x => c x / d x) x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>hc : DifferentiableOn 𝕜 c s<VAR>hd : DifferentiableOn 𝕜 d s<VAR>hx : ∀ x ∈ s, d x ≠ 0<GOAL>DifferentiableOn 𝕜 (fun x => c x / d x) s
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>hc : Differentiable 𝕜 c<VAR>hd : Differentiable 𝕜 d<VAR>hx : ∀ (x : 𝕜), d x ≠ 0<GOAL>Differentiable 𝕜 fun x => c x / d x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>hc : DifferentiableWithinAt 𝕜 c s x<VAR>hd : DifferentiableWithinAt 𝕜 d s x<VAR>hx : d x ≠ 0<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun x => c x / d x) s x = (derivWithin c s x * d x - c x * derivWithin d s x) / d x ^ 2
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>x : 𝕜<VAR>𝕜' : Type u_1<VAR>NontriviallyNormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>c d : 𝕜 → 𝕜'<VAR>hc : DifferentiableAt 𝕜 c x<VAR>hd : DifferentiableAt 𝕜 d x<VAR>hx : d x ≠ 0<GOAL>deriv (fun x => c x / d x) x = (deriv c x * d x - c x * deriv d x) / d x ^ 2
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>StarAddMonoid F<VAR>ContinuousStar F<VAR>StarModule 𝕜 F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<VAR>h : HasDerivAtFilter f f' x L<GOAL>HasDerivAtFilter (fun x => star (f x)) (star f') x L
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>StarAddMonoid F<VAR>ContinuousStar F<VAR>StarModule 𝕜 F<VAR>f' : F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>h : HasDerivWithinAt f f' s x<GOAL>HasDerivWithinAt (fun x => star (f x)) (star f') s x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>StarAddMonoid F<VAR>ContinuousStar F<VAR>StarModule 𝕜 F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasDerivAt f f' x<GOAL>HasDerivAt (fun x => star (f x)) (star f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>StarAddMonoid F<VAR>ContinuousStar F<VAR>StarModule 𝕜 F<VAR>f' : F<VAR>x : 𝕜<VAR>h : HasStrictDerivAt f f' x<GOAL>HasStrictDerivAt (fun x => star (f x)) (star f') x
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>StarAddMonoid F<VAR>ContinuousStar F<VAR>StarModule 𝕜 F<VAR>s : Set 𝕜<VAR>x : 𝕜<VAR>hxs : UniqueDiffWithinAt 𝕜 s x<GOAL>derivWithin (fun y => star (f y)) s x = star (derivWithin f s x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>StarAddMonoid F<VAR>ContinuousStar F<VAR>StarModule 𝕜 F<VAR>x : 𝕜<GOAL>deriv (fun y => star (f y)) x = star (deriv f x)
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>StarRing 𝕜<VAR>TrivialStar 𝕜<VAR>StarAddMonoid F<VAR>ContinuousStar F<VAR>StarModule 𝕜 F<GOAL>(deriv fun y => star (f y)) = fun x => star (deriv f x)
<VAR>E : Type u_1<VAR>c : E<VAR>self : ContDiffBump c<GOAL>0 < self.rIn
<VAR>E : Type u_1<VAR>c : E<VAR>self : ContDiffBump c<GOAL>self.rIn < self.rOut
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>self : ContDiffBumpBase E<VAR>R : ℝ<GOAL>1 < R → Function.support (self.toFun R) = Metric.ball 0 R
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>self : ContDiffBumpBase E<GOAL>ContDiffOn ℝ ⊤ (Function.uncurry self.toFun) (Set.Ioi 1 ×ˢ Set.univ)
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>self : ContDiffBumpBase E<VAR>R : ℝ<GOAL>1 < R → ∀ (x : E), ‖x‖ ≤ 1 → self.toFun R x = 1
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>self : ContDiffBumpBase E<VAR>R : ℝ<VAR>x : E<GOAL>self.toFun R (-x) = self.toFun R x
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>self : ContDiffBumpBase E<VAR>R : ℝ<VAR>x : E<GOAL>self.toFun R x ∈ Set.Icc 0 1
<VAR>E : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>self : HasContDiffBump E<GOAL>Nonempty (ContDiffBumpBase E)
<VAR>E : Type u_1<VAR>c : E<VAR>f : ContDiffBump c<GOAL>0 < f.rOut
<VAR>E : Type u_1<VAR>c : E<VAR>f : ContDiffBump c<GOAL>1 < f.rOut / f.rIn
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<GOAL>↑f x = (someContDiffBumpBase E).toFun (f.rOut / f.rIn) (f.rIn⁻¹ • (x - c))
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<GOAL>↑f (c - x) = ↑f (c + x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>f : ContDiffBump 0<VAR>x : E<GOAL>↑f (-x) = ↑f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>hx : x ∈ Metric.closedBall c f.rIn<GOAL>↑f x = 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<GOAL>0 ≤ ↑f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<GOAL>↑f x ≤ 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<GOAL>Function.support ↑f = Metric.ball c f.rOut
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<GOAL>tsupport ↑f = Metric.closedBall c f.rOut
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>hx : x ∈ Metric.ball c f.rOut<GOAL>0 < ↑f x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>hx : f.rOut ≤ dist x c<GOAL>↑f x = 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>FiniteDimensional ℝ E<GOAL>HasCompactSupport ↑f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>h : x ∈ Metric.ball c f.rIn<GOAL>↑f =ᶠ[𝓝 x] 1
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<GOAL>↑f =ᶠ[𝓝 c] 1
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<VAR>HasContDiffBump E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>s : Set X<VAR>f : (x : X) → ContDiffBump (c x)<VAR>x : X<VAR>hc : ContDiffWithinAt ℝ n c s x<VAR>hr : ContDiffWithinAt ℝ n (fun x => (f x).rIn) s x<VAR>hR : ContDiffWithinAt ℝ n (fun x => (f x).rOut) s x<VAR>hg : ContDiffWithinAt ℝ n g s x<GOAL>ContDiffWithinAt ℝ n (fun x => ↑(f x) (g x)) s x
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<VAR>HasContDiffBump E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>f : (x : X) → ContDiffBump (c x)<VAR>x : X<VAR>hc : ContDiffAt ℝ n c x<VAR>hr : ContDiffAt ℝ n (fun x => (f x).rIn) x<VAR>hR : ContDiffAt ℝ n (fun x => (f x).rOut) x<VAR>hg : ContDiffAt ℝ n g x<GOAL>ContDiffAt ℝ n (fun x => ↑(f x) (g x)) x
<VAR>E : Type u_1<VAR>X : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup X<VAR>NormedSpace ℝ X<VAR>HasContDiffBump E<VAR>n : ℕ∞<VAR>c g : X → E<VAR>f : (x : X) → ContDiffBump (c x)<VAR>hc : ContDiff ℝ n c<VAR>hr : ContDiff ℝ n fun x => (f x).rIn<VAR>hR : ContDiff ℝ n fun x => (f x).rOut<VAR>hg : ContDiff ℝ n g<GOAL>ContDiff ℝ n fun x => ↑(f x) (g x)
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>n : ℕ∞<GOAL>ContDiff ℝ n ↑f
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n (↑f) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<VAR>x : E<VAR>n : ℕ∞<VAR>s : Set E<GOAL>ContDiffWithinAt ℝ n (↑f) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>HasContDiffBump E<VAR>c : E<VAR>f : ContDiffBump c<GOAL>Continuous ↑f
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>L : Filter 𝕜<GOAL>HasDerivAtFilter f f' x L ↔ Filter.Tendsto (slope f x) (L ⊓ 𝓟 {x}ᶜ) (𝓝 f')
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<GOAL>HasDerivWithinAt f f' s x ↔ Filter.Tendsto (slope f x) (𝓝[s \ {x}] x) (𝓝 f')
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>s : Set 𝕜<VAR>hs : x ∉ s<GOAL>HasDerivWithinAt f f' s x ↔ Filter.Tendsto (slope f x) (𝓝[s] x) (𝓝 f')
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<GOAL>HasDerivAt f f' x ↔ Filter.Tendsto (slope f x) (𝓝[≠] x) (𝓝 f')
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<GOAL>HasDerivAt f f' x ↔ Filter.Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[≠] 0) (𝓝 f')
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>PartialOrder 𝕜<VAR>h : HasDerivAt f f' x<GOAL>Filter.Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[>] 0) (𝓝 f')
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>f' : F<VAR>x : 𝕜<VAR>PartialOrder 𝕜<VAR>h : HasDerivAt f f' x<GOAL>Filter.Tendsto (fun t => t⁻¹ • (f (x + t) - f x)) (𝓝[<] 0) (𝓝 f')
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>s t : Set 𝕜<VAR>h : s ⊆ closure (s ∩ t)<GOAL>Set.range (derivWithin f s) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>f : 𝕜 → F<VAR>t : Set 𝕜<VAR>h : Dense t<GOAL>Set.range (deriv f) ⊆ closure ↑(Submodule.span 𝕜 (f '' t))
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace.SeparableSpace 𝕜<VAR>f : 𝕜 → F<VAR>s : Set 𝕜<GOAL>TopologicalSpace.IsSeparable (Set.range (derivWithin f s))
<VAR>𝕜 : Type u<VAR>NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>TopologicalSpace.SeparableSpace 𝕜<VAR>f : 𝕜 → F<GOAL>TopologicalSpace.IsSeparable (Set.range (deriv f))
<VAR>f : ℝ → ℝ<VAR>f' : ℝ<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : f' < r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s \ {x}] x, slope f x z < r
<VAR>f : ℝ → ℝ<VAR>f' : ℝ<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hs : x ∉ s<VAR>hr : f' < r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, slope f x z < r
<VAR>f : ℝ → ℝ<VAR>f' x r : ℝ<VAR>hf : HasDerivWithinAt f f' (Set.Ici x) x<VAR>hr : f' < r<GOAL>∃ᶠ (z : ℝ) in 𝓝[>] x, slope f x z < r
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>s : Set ℝ<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hr : ‖f'‖ < r<GOAL>∀ᶠ (z : ℝ) in 𝓝[s] x, ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' (Set.Ici x) x<VAR>hr : ‖f'‖ < r<GOAL>∃ᶠ (z : ℝ) in 𝓝[>] x, ‖z - x‖⁻¹ * ‖f z - f x‖ < r
<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : ℝ → E<VAR>f' : E<VAR>x r : ℝ<VAR>hf : HasDerivWithinAt f f' (Set.Ici x) x<VAR>hr : ‖f'‖ < r<GOAL>∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
<VAR>𝕜 : Type u_1<VAR>ι : Type u_2<VAR>E : ι → Type u_3<VAR>F : Type u_4<VAR>NormedField 𝕜<VAR>Finite ι<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>TopologicalSpace F<VAR>AddCommGroup F<VAR>TopologicalAddGroup F<VAR>Module 𝕜 F<GOAL>Continuous fun p => p.1 p.2
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>hf : Continuous ⇑f<VAR>m : (i : ι) → E i<VAR>i : ι<VAR>hi : ‖m i‖ = 0<GOAL>‖f m‖ = 0
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>hf₀ : ∀ {m : (i : ι) → E i} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0<VAR>ε : ι → ℝ<VAR>C : ℝ<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>c : ι → 𝕜<VAR>hc : ∀ (i : ι), 1 < ‖c i‖<VAR>hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m : (i : ι) → E i<GOAL>‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>hfc : Continuous ⇑f<VAR>ε : ι → ℝ<VAR>C : ℝ<VAR>hε : ∀ (i : ι), 0 < ε i<VAR>c : ι → 𝕜<VAR>hc : ∀ (i : ι), 1 < ‖c i‖<VAR>hf : ∀ (m : (i : ι) → E i), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m : (i : ι) → E i<GOAL>‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>hf : Continuous ⇑f<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>DecidableEq ι<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m₁ m₂ : (i : ι) → E i<GOAL>‖f m₁ - f m₂‖ ≤ C * ∑ i : ι, ∏ j : ι, if j = i then ‖m₁ i - m₂ i‖ else max ‖m₁ j‖ ‖m₂ j‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>hC : 0 ≤ C<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<VAR>m₁ m₂ : (i : ι) → E i<GOAL>‖f m₁ - f m₂‖ ≤ C * ↑(Fintype.card ι) * max ‖m₁‖ ‖m₂‖ ^ (Fintype.card ι - 1) * ‖m₁ - m₂‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<GOAL>Continuous ⇑f
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : MultilinearMap 𝕜 E G<VAR>C : ℝ<VAR>H : ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖<GOAL>⇑(f.mkContinuous C H) = ⇑f
<VAR>𝕜 : Type u<VAR>G : Type wG<VAR>G' : Type wG'<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>SeminormedAddCommGroup G'<VAR>NormedSpace 𝕜 G'<VAR>k n : ℕ<VAR>f : MultilinearMap 𝕜 (fun x => G) G'<VAR>s : Finset (Fin n)<VAR>hk : s.card = k<VAR>z : G<VAR>C : ℝ<VAR>H : ∀ (m : Fin n → G), ‖f m‖ ≤ C * ∏ i : Fin n, ‖m i‖<VAR>v : Fin k → G<GOAL>‖(f.restr s hk z) v‖ ≤ C * ‖z‖ ^ (n - k) * ∏ i : Fin k, ‖v i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>∃ C, 0 < C ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ C * ∏ i : ι, ‖m i‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>‖f‖ = sInf {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>∃ c, c ∈ {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>BddBelow {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖}
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>IsLeast {c | 0 ≤ c ∧ ∀ (m : (i : ι) → E i), ‖f m‖ ≤ c * ∏ i : ι, ‖m i‖} ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<GOAL>0 ≤ ‖f‖
<VAR>𝕜 : Type u<VAR>ι : Type v<VAR>E : ι → Type wE<VAR>G : Type wG<VAR>Fintype ι<VAR>NontriviallyNormedField 𝕜<VAR>(i : ι) → SeminormedAddCommGroup (E i)<VAR>(i : ι) → NormedSpace 𝕜 (E i)<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 G<VAR>f : ContinuousMultilinearMap 𝕜 E G<VAR>m : (i : ι) → E i<GOAL>‖f m‖ ≤ ‖f‖ * ∏ i : ι, ‖m i‖