ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>p : ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>h : f x ≠ 0 ∨ 1 ≤ p<GOAL>DifferentiableWithinAt ℝ (fun x => f x ^ p) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>p : ℝ<VAR>hf : DifferentiableAt ℝ f x<VAR>h : f x ≠ 0 ∨ 1 ≤ p<GOAL>DifferentiableAt ℝ (fun x => f x ^ p) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>p : ℝ<VAR>hf : DifferentiableOn ℝ f s<VAR>h : ∀ x ∈ s, f x ≠ 0 ∨ 1 ≤ p<GOAL>DifferentiableOn ℝ (fun x => f x ^ p) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>p : ℝ<VAR>hf : Differentiable ℝ f<VAR>h : ∀ (x : E), f x ≠ 0 ∨ 1 ≤ p<GOAL>Differentiable ℝ fun x => f x ^ p
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>c : ℝ<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hc : 0 < c<GOAL>HasFDerivWithinAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>c : ℝ<VAR>hf : HasFDerivAt f f' x<VAR>hc : 0 < c<GOAL>HasFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>c : ℝ<VAR>hf : HasStrictFDerivAt f f' x<VAR>hc : 0 < c<GOAL>HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Real.log c) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>hg : ContDiffWithinAt ℝ n g s x<VAR>h : f x ≠ 0<GOAL>ContDiffWithinAt ℝ n (fun x => f x ^ g x) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>x : E<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<VAR>hg : ContDiffAt ℝ n g x<VAR>h : f x ≠ 0<GOAL>ContDiffAt ℝ n (fun x => f x ^ g x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>s : Set E<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<VAR>hg : ContDiffOn ℝ n g s<VAR>h : ∀ x ∈ s, f x ≠ 0<GOAL>ContDiffOn ℝ n (fun x => f x ^ g x) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>hg : ContDiff ℝ n g<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>ContDiff ℝ n fun x => f x ^ g x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>p : ℝ<VAR>n : ℕ∞<VAR>hf : ContDiffWithinAt ℝ n f s x<VAR>h : f x ≠ 0<GOAL>ContDiffWithinAt ℝ n (fun x => f x ^ p) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>p : ℝ<VAR>n : ℕ∞<VAR>hf : ContDiffAt ℝ n f x<VAR>h : f x ≠ 0<GOAL>ContDiffAt ℝ n (fun x => f x ^ p) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>p : ℝ<VAR>n : ℕ∞<VAR>hf : ContDiffOn ℝ n f s<VAR>h : ∀ x ∈ s, f x ≠ 0<GOAL>ContDiffOn ℝ n (fun x => f x ^ p) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>p : ℝ<VAR>n : ℕ∞<VAR>hf : ContDiff ℝ n f<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>ContDiff ℝ n fun x => f x ^ p
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>p : ℝ<VAR>m : ℕ<VAR>hf : ContDiffWithinAt ℝ (↑m) f s x<VAR>h : ↑m ≤ p<GOAL>ContDiffWithinAt ℝ (↑m) (fun x => f x ^ p) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>x : E<VAR>p : ℝ<VAR>m : ℕ<VAR>hf : ContDiffAt ℝ (↑m) f x<VAR>h : ↑m ≤ p<GOAL>ContDiffAt ℝ (↑m) (fun x => f x ^ p) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>s : Set E<VAR>p : ℝ<VAR>m : ℕ<VAR>hf : ContDiffOn ℝ (↑m) f s<VAR>h : ↑m ≤ p<GOAL>ContDiffOn ℝ (↑m) (fun x => f x ^ p) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>p : ℝ<VAR>m : ℕ<VAR>hf : ContDiff ℝ (↑m) f<VAR>h : ↑m ≤ p<GOAL>ContDiff ℝ ↑m fun x => f x ^ p
<VAR>f g : ℝ → ℝ<VAR>f' g' x : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<VAR>h : 0 < f x<GOAL>HasDerivWithinAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) s x
<VAR>f g : ℝ → ℝ<VAR>f' g' x : ℝ<VAR>hf : HasDerivAt f f' x<VAR>hg : HasDerivAt g g' x<VAR>h : 0 < f x<GOAL>HasDerivAt (fun x => f x ^ g x) (f' * g x * f x ^ (g x - 1) + g' * f x ^ g x * Real.log (f x)) x
<VAR>f : ℝ → ℝ<VAR>f' x p : ℝ<VAR>s : Set ℝ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hx : f x ≠ 0 ∨ 1 ≤ p<GOAL>HasDerivWithinAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) s x
<VAR>f : ℝ → ℝ<VAR>f' x p : ℝ<VAR>hf : HasDerivAt f f' x<VAR>hx : f x ≠ 0 ∨ 1 ≤ p<GOAL>HasDerivAt (fun y => f y ^ p) (f' * p * f x ^ (p - 1)) x
<VAR>f : ℝ → ℝ<VAR>x p : ℝ<VAR>s : Set ℝ<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hx : f x ≠ 0 ∨ 1 ≤ p<VAR>hxs : UniqueDiffWithinAt ℝ s x<GOAL>derivWithin (fun x => f x ^ p) s x = derivWithin f s x * p * f x ^ (p - 1)
<VAR>f : ℝ → ℝ<VAR>x p : ℝ<VAR>hf : DifferentiableAt ℝ f x<VAR>hx : f x ≠ 0 ∨ 1 ≤ p<GOAL>deriv (fun x => f x ^ p) x = deriv f x * p * f x ^ (p - 1)
<VAR>p : ℝ<VAR>hp : p ≠ 0<GOAL>(deriv fun x => x ^ p) =Θ[Filter.atTop] fun x => x ^ (p - 1)
<VAR>p : ℝ<GOAL>(deriv fun x => x ^ p) =O[Filter.atTop] fun x => x ^ (p - 1)
<VAR>t : ℝ<GOAL>Filter.Tendsto (fun x => (1 + t / x) ^ x) Filter.atTop (𝓝 (rexp t))
<VAR>t : ℝ<GOAL>Filter.Tendsto (fun x => (1 + t / ↑x) ^ x) Filter.atTop (𝓝 (rexp t))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>x y : 𝕜'<GOAL>((ContinuousLinearMap.mul 𝕜 𝕜') x) y = x * y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>x : 𝕜'<GOAL>‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖ ≤ ‖x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<GOAL>‖ContinuousLinearMap.mul 𝕜 𝕜'‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<GOAL>⇑(NonUnitalAlgHom.Lmul 𝕜 𝕜') = ⇑(ContinuousLinearMap.mul 𝕜 𝕜')
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>x y z : 𝕜'<GOAL>(((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y) z = x * z * y
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>x y : 𝕜'<GOAL>‖((ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x) y‖ ≤ ‖x‖ * ‖y‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>x : 𝕜'<GOAL>‖(ContinuousLinearMap.mulLeftRight 𝕜 𝕜') x‖ ≤ ‖x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<GOAL>‖ContinuousLinearMap.mulLeftRight 𝕜 𝕜'‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>self : RegularNormedAlgebra 𝕜 𝕜'<GOAL>Isometry ⇑(ContinuousLinearMap.mul 𝕜 𝕜')
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>RegularNormedAlgebra 𝕜 𝕜'<GOAL>Isometry ⇑(ContinuousLinearMap.mul 𝕜 𝕜')
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>RegularNormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜'<GOAL>‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>RegularNormedAlgebra 𝕜 𝕜'<VAR>x : 𝕜'<GOAL>‖(ContinuousLinearMap.mul 𝕜 𝕜') x‖₊ = ‖x‖₊
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalSeminormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>RegularNormedAlgebra 𝕜 𝕜'<GOAL>⇑(ContinuousLinearMap.mulₗᵢ 𝕜 𝕜') = ⇑(ContinuousLinearMap.mul 𝕜 𝕜')
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>c : 𝕜'<VAR>x : E<GOAL>((ContinuousLinearMap.lsmul 𝕜 𝕜') c) x = c • x
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>‖ContinuousLinearMap.toSpanSingleton 𝕜 x‖ = ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>x : 𝕜'<GOAL>‖(ContinuousLinearMap.lsmul 𝕜 𝕜') x‖ ≤ ‖x‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<GOAL>‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalNormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>RegularNormedAlgebra 𝕜 𝕜'<VAR>Nontrivial 𝕜'<GOAL>‖ContinuousLinearMap.mul 𝕜 𝕜'‖ = 1
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>𝕜' : Type u_3<VAR>NonUnitalNormedRing 𝕜'<VAR>NormedSpace 𝕜 𝕜'<VAR>IsScalarTower 𝕜 𝕜' 𝕜'<VAR>SMulCommClass 𝕜 𝕜' 𝕜'<VAR>RegularNormedAlgebra 𝕜 𝕜'<VAR>Nontrivial 𝕜'<GOAL>‖ContinuousLinearMap.mul 𝕜 𝕜'‖₊ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>𝕜' : Type u_3<VAR>NormedField 𝕜'<VAR>NormedAlgebra 𝕜 𝕜'<VAR>NormedSpace 𝕜' E<VAR>IsScalarTower 𝕜 𝕜' E<VAR>Nontrivial E<GOAL>‖ContinuousLinearMap.lsmul 𝕜 𝕜'‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<GOAL>‖ContinuousLinearMap.fst 𝕜 E F‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<GOAL>‖ContinuousLinearMap.snd 𝕜 E F‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F<VAR>g : E →L[𝕜] G<GOAL>‖f.prod g‖ = ‖(f, g)‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>G : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>SeminormedAddCommGroup G<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>NormedSpace 𝕜 G<VAR>f : E →L[𝕜] F<VAR>g : E →L[𝕜] G<GOAL>‖f.prod g‖₊ = ‖(f, g)‖₊
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>M₄ : Type u_8<VAR>SeminormedAddCommGroup M₁<VAR>NormedSpace 𝕜 M₁<VAR>SeminormedAddCommGroup M₂<VAR>NormedSpace 𝕜 M₂<VAR>SeminormedAddCommGroup M₃<VAR>NormedSpace 𝕜 M₃<VAR>SeminormedAddCommGroup M₄<VAR>NormedSpace 𝕜 M₄<VAR>p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)<GOAL>(ContinuousLinearMap.prodMapL 𝕜 M₁ M₂ M₃ M₄) p = p.1.prodMap p.2
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>M₄ : Type u_8<VAR>SeminormedAddCommGroup M₁<VAR>NormedSpace 𝕜 M₁<VAR>SeminormedAddCommGroup M₂<VAR>NormedSpace 𝕜 M₂<VAR>SeminormedAddCommGroup M₃<VAR>NormedSpace 𝕜 M₃<VAR>SeminormedAddCommGroup M₄<VAR>NormedSpace 𝕜 M₄<VAR>X : Type u_9<VAR>TopologicalSpace X<VAR>f : X → M₁ →L[𝕜] M₂<VAR>g : X → M₃ →L[𝕜] M₄<VAR>hf : Continuous f<VAR>hg : Continuous g<GOAL>Continuous fun x => (f x).prodMap (g x)
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>M₄ : Type u_8<VAR>SeminormedAddCommGroup M₁<VAR>NormedSpace 𝕜 M₁<VAR>SeminormedAddCommGroup M₂<VAR>NormedSpace 𝕜 M₂<VAR>SeminormedAddCommGroup M₃<VAR>NormedSpace 𝕜 M₃<VAR>SeminormedAddCommGroup M₄<VAR>NormedSpace 𝕜 M₄<VAR>X : Type u_9<VAR>TopologicalSpace X<VAR>f : X → M₁ ≃L[𝕜] M₂<VAR>g : X → M₃ ≃L[𝕜] M₄<VAR>hf : Continuous fun x => ↑(f x)<VAR>hg : Continuous fun x => ↑(g x)<GOAL>Continuous fun x => ↑((f x).prod (g x))
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>M₄ : Type u_8<VAR>SeminormedAddCommGroup M₁<VAR>NormedSpace 𝕜 M₁<VAR>SeminormedAddCommGroup M₂<VAR>NormedSpace 𝕜 M₂<VAR>SeminormedAddCommGroup M₃<VAR>NormedSpace 𝕜 M₃<VAR>SeminormedAddCommGroup M₄<VAR>NormedSpace 𝕜 M₄<VAR>X : Type u_9<VAR>TopologicalSpace X<VAR>f : X → M₁ →L[𝕜] M₂<VAR>g : X → M₃ →L[𝕜] M₄<VAR>s : Set X<VAR>hf : ContinuousOn f s<VAR>hg : ContinuousOn g s<GOAL>ContinuousOn (fun x => (f x).prodMap (g x)) s
<VAR>𝕜 : Type u_1<VAR>NontriviallyNormedField 𝕜<VAR>M₁ : Type u_5<VAR>M₂ : Type u_6<VAR>M₃ : Type u_7<VAR>M₄ : Type u_8<VAR>SeminormedAddCommGroup M₁<VAR>NormedSpace 𝕜 M₁<VAR>SeminormedAddCommGroup M₂<VAR>NormedSpace 𝕜 M₂<VAR>SeminormedAddCommGroup M₃<VAR>NormedSpace 𝕜 M₃<VAR>SeminormedAddCommGroup M₄<VAR>NormedSpace 𝕜 M₄<VAR>X : Type u_9<VAR>TopologicalSpace X<VAR>f : X → M₁ ≃L[𝕜] M₂<VAR>g : X → M₃ ≃L[𝕜] M₄<VAR>s : Set X<VAR>hf : ContinuousOn (fun x => ↑(f x)) s<VAR>hg : ContinuousOn (fun x => ↑(g x)) s<GOAL>ContinuousOn (fun x => ↑((f x).prod (g x))) s
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Nontrivial E<GOAL>‖ContinuousLinearMap.fst 𝕜 E F‖ = 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NontriviallyNormedField 𝕜<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>Nontrivial F<GOAL>‖ContinuousLinearMap.snd 𝕜 E F‖ = 1
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>hs₀ : 0 ∈ s<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>x₀ : E<VAR>hx₀ : x₀ ∉ s<GOAL>∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht : Convex ℝ t<VAR>disj : Disjoint s t<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u ≤ f b
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>disj : x ∉ s<GOAL>∃ f, ∀ a ∈ s, f a < f x
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>t : Set E<VAR>x : E<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsOpen t<VAR>disj : x ∉ t<GOAL>∃ f, ∀ b ∈ t, f x < f b
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsOpen s<VAR>ht₁ : Convex ℝ t<VAR>ht₃ : IsOpen t<VAR>disj : Disjoint s t<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ ∀ b ∈ t, u < f b
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsCompact s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : Disjoint s t<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s t : Set E<VAR>LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsClosed s<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsCompact t<VAR>disj : Disjoint s t<GOAL>∃ f u v, (∀ a ∈ s, f a < u) ∧ u < v ∧ ∀ b ∈ t, v < f b
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>t : Set E<VAR>x : E<VAR>LocallyConvexSpace ℝ E<VAR>ht₁ : Convex ℝ t<VAR>ht₂ : IsClosed t<VAR>disj : x ∉ t<GOAL>∃ f u, f x < u ∧ ∀ b ∈ t, u < f b
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>x : E<VAR>LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsClosed s<VAR>disj : x ∉ s<GOAL>∃ f u, (∀ a ∈ s, f a < u) ∧ u < f x
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>x y : E<VAR>LocallyConvexSpace ℝ E<VAR>T1Space E<VAR>hxy : x ≠ y<GOAL>∃ f, f x < f y
<VAR>E : Type u_2<VAR>TopologicalSpace E<VAR>AddCommGroup E<VAR>TopologicalAddGroup E<VAR>Module ℝ E<VAR>ContinuousSMul ℝ E<VAR>s : Set E<VAR>LocallyConvexSpace ℝ E<VAR>hs₁ : Convex ℝ s<VAR>hs₂ : IsClosed s<GOAL>⋂ l, {x | ∃ y ∈ s, l x ≤ l y} = s
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<GOAL>‖x‖⁻¹ • x ∈ Metric.closedBall 0 1
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>t : ℝ<VAR>ht : 0 ≤ t<VAR>x : E<GOAL>‖t • x‖ = t * ‖x‖
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>r : ℝ<VAR>x y : E<VAR>h : r ∈ Set.Icc 0 1<GOAL>dist (r • x + (1 - r) • y) x ≤ dist y x
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>closure (Metric.ball x r) = Metric.closedBall x r
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>frontier (Metric.ball x r) = Metric.sphere x r
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>interior (Metric.closedBall x r) = Metric.ball x r
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>frontier (Metric.closedBall x r) = Metric.sphere x r
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>interior (Metric.sphere x r) = ∅
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : E<VAR>r : ℝ<VAR>hr : r ≠ 0<GOAL>frontier (Metric.sphere x r) = Metric.sphere x r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>c : ℝ<VAR>hc : 0 ≤ c<GOAL>∃ x, ‖x‖ = c
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<GOAL>Set.range norm = Set.Ici 0
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<GOAL>Function.Surjective nnnorm
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<GOAL>Set.range nnnorm = Set.univ
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>interior (Metric.closedBall x r) = Metric.ball x r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>frontier (Metric.closedBall x r) = Metric.sphere x r
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>interior (Metric.sphere x r) = ∅
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>Nontrivial E<VAR>x : E<VAR>r : ℝ<GOAL>frontier (Metric.sphere x r) = Metric.sphere x r
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalSpace R<VAR>Module R V<GOAL>SeparatingDual R V ↔ ∀ (x : V), x ≠ 0 → ∃ f, f x ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalSpace R<VAR>Module R V<VAR>self : SeparatingDual R V<VAR>x : V<GOAL>x ≠ 0 → ∃ f, f x ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalSpace R<VAR>Module R V<VAR>SeparatingDual R V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>∃ f, f x ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalSpace R<VAR>Module R V<VAR>SeparatingDual R V<VAR>x y : V<VAR>h : x ≠ y<GOAL>∃ f, f x ≠ f y
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalSpace R<VAR>Module R V<VAR>SeparatingDual R V<VAR>T1Space R<GOAL>T1Space V
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Ring R<VAR>AddCommGroup V<VAR>TopologicalSpace V<VAR>TopologicalSpace R<VAR>Module R V<VAR>SeparatingDual R V<VAR>T2Space R<GOAL>T2Space V
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Field R<VAR>AddCommGroup V<VAR>TopologicalSpace R<VAR>TopologicalSpace V<VAR>TopologicalRing R<VAR>Module R V<GOAL>SeparatingDual R V ↔ Function.Injective ⇑(ContinuousLinearMap.coeLM R).flip
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Field R<VAR>AddCommGroup V<VAR>TopologicalSpace R<VAR>TopologicalSpace V<VAR>TopologicalRing R<VAR>Module R V<VAR>SeparatingDual R V<VAR>W : Type u_3<VAR>AddCommGroup W<VAR>Module R W<VAR>FiniteDimensional R W<VAR>f : W →ₗ[R] V<GOAL>Function.Surjective (⇑f.dualMap ∘ ContinuousLinearMap.toLinearMap) ↔ Function.Injective ⇑f
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Field R<VAR>AddCommGroup V<VAR>TopologicalSpace R<VAR>TopologicalSpace V<VAR>TopologicalRing R<VAR>Module R V<VAR>SeparatingDual R V<VAR>x : V<VAR>hx : x ≠ 0<GOAL>∃ f, f x = 1
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Field R<VAR>AddCommGroup V<VAR>TopologicalSpace R<VAR>TopologicalSpace V<VAR>TopologicalRing R<VAR>Module R V<VAR>SeparatingDual R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ f, f x = 1 ∧ f y ≠ 0
<VAR>R : Type u_1<VAR>V : Type u_2<VAR>Field R<VAR>AddCommGroup V<VAR>TopologicalSpace R<VAR>TopologicalSpace V<VAR>TopologicalRing R<VAR>TopologicalAddGroup V<VAR>Module R V<VAR>SeparatingDual R V<VAR>ContinuousSMul R V<VAR>x y : V<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>∃ A, A x = y
<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>SeparatingDual 𝕜 E<VAR>Nontrivial E<VAR>CompleteSpace (E →L[𝕜] F)<GOAL>CompleteSpace F
<VAR>𝕜 : Type u_3<VAR>E : Type u_4<VAR>F : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>SeparatingDual 𝕜 E<VAR>Nontrivial E<GOAL>CompleteSpace (E →L[𝕜] F) ↔ CompleteSpace F
<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_6<VAR>Finite ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>CompleteSpace (ContinuousMultilinearMap 𝕜 M F)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<GOAL>CompleteSpace F
<VAR>𝕜 : Type u_3<VAR>F : Type u_5<VAR>NontriviallyNormedField 𝕜<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>ι : Type u_6<VAR>Finite ι<VAR>M : ι → Type u_7<VAR>(i : ι) → NormedAddCommGroup (M i)<VAR>(i : ι) → NormedSpace 𝕜 (M i)<VAR>∀ (i : ι), SeparatingDual 𝕜 (M i)<VAR>m : (i : ι) → M i<VAR>hm : ∀ (i : ι), m i ≠ 0<GOAL>CompleteSpace (ContinuousMultilinearMap 𝕜 M F) ↔ CompleteSpace F
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : ↑{0}ᶜ<GOAL>↑((homeomorphUnitSphereProd E) x).2 = ‖↑x‖
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : ↑{0}ᶜ<GOAL>↑((homeomorphUnitSphereProd E) x).1 = ‖↑x‖⁻¹ • ↑x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>x : ↑(Metric.sphere 0 1) × ↑(Set.Ioi 0)<GOAL>↑((homeomorphUnitSphereProd E).symm x) = ↑x.2 • ↑x.1
<VAR>u : ℂ<VAR>hu : 0 < u.re<VAR>v : ℂ<GOAL>IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 (1 / 2)
<VAR>u v : ℂ<VAR>hu : 0 < u.re<VAR>hv : 0 < v.re<GOAL>IntervalIntegrable (fun x => ↑x ^ (u - 1) * (1 - ↑x) ^ (v - 1)) MeasureTheory.volume 0 1
<VAR>u v : ℂ<GOAL>v.betaIntegral u = u.betaIntegral v