ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>P : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>Nontrivial ι<VAR>b : AffineBasis ι 𝕜 P<VAR>i : ι<GOAL>IsOpenMap ⇑(b.coord i)
<VAR>ι : Type u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>P : Type u_4<VAR>NontriviallyNormedField 𝕜<VAR>CompleteSpace 𝕜<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>MetricSpace P<VAR>NormedAddTorsor E P<VAR>FiniteDimensional 𝕜 E<VAR>b : AffineBasis ι 𝕜 P<VAR>i : ι<GOAL>Continuous ⇑(b.coord i)
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>Finite ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : AffineBasis ι ℝ E<GOAL>interior ((convexHull ℝ) (Set.range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>s u : Set P<VAR>hu : IsOpen u<VAR>hsu : s ⊆ u<VAR>hne : s.Nonempty<VAR>h : AffineIndependent ℝ Subtype.val<GOAL>∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>u : Set P<VAR>hu : IsOpen u<VAR>hne : u.Nonempty<GOAL>∃ s ⊆ u, AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ s = ⊤
<VAR>V : Type u_1<VAR>P : Type u_2<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>u : Set P<VAR>hu : IsOpen u<VAR>hne : u.Nonempty<GOAL>affineSpan ℝ u = ⊤
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>s : Set V<VAR>hs : (interior ((convexHull ℝ) s)).Nonempty<GOAL>affineSpan ℝ s = ⊤
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>ι : Type u_3<VAR>Fintype ι<VAR>b : AffineBasis ι ℝ V<GOAL>Finset.centroid ℝ Finset.univ ⇑b ∈ interior ((convexHull ℝ) (Set.range ⇑b))
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>s : Set V<GOAL>(interior ((convexHull ℝ) s)).Nonempty ↔ affineSpan ℝ s = ⊤
<VAR>V : Type u_1<VAR>NormedAddCommGroup V<VAR>NormedSpace ℝ V<VAR>FiniteDimensional ℝ V<VAR>s : Set V<VAR>hs : Convex ℝ s<GOAL>(interior s).Nonempty ↔ affineSpan ℝ s = ⊤
<VAR>x : ℂ<GOAL>Real.sin x.arg = x.im / Complex.abs x
<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>Real.cos x.arg = x.re / Complex.abs x
<VAR>x : ℂ<GOAL>↑(Complex.abs x) * Complex.exp (↑x.arg * Complex.I) = x
<VAR>x : ℂ<GOAL>↑(Complex.abs x) * (Complex.cos ↑x.arg + Complex.sin ↑x.arg * Complex.I) = x
<VAR>x : ℂ<GOAL>Complex.abs x * Real.cos x.arg = x.re
<VAR>x : ℂ<GOAL>Complex.abs x * Real.sin x.arg = x.im
<VAR>z : ℂ<GOAL>Complex.abs z = 1 ↔ ∃ θ, Complex.exp (↑θ * Complex.I) = z
<GOAL>(Set.range fun x => Complex.exp (↑x * Complex.I)) = Metric.sphere 0 1
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<VAR>hθ : θ ∈ Set.Ioc (-π) π<GOAL>(↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg = θ
<VAR>θ : ℝ<VAR>hθ : θ ∈ Set.Ioc (-π) π<GOAL>(Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg = θ
<VAR>θ : ℝ<GOAL>(Complex.exp (↑θ * Complex.I)).arg = toIocMod ⋯ (-π) θ
<VAR>x y : ℂ<VAR>h₁ : Complex.abs x = Complex.abs y<VAR>h₂ : x.arg = y.arg<GOAL>x = y
<VAR>x y : ℂ<GOAL>x = y ↔ Complex.abs x = Complex.abs y ∧ x.arg = y.arg
<VAR>z : ℂ<GOAL>z.arg ∈ Set.Ioc (-π) π
<VAR>z : ℂ<GOAL>|z.arg| ≤ π
<VAR>z : ℂ<GOAL>0 ≤ z.arg ↔ 0 ≤ z.im
<VAR>z : ℂ<GOAL>z.arg < 0 ↔ z.im < 0
<VAR>x : ℂ<VAR>r : ℝ<VAR>hr : 0 < r<GOAL>(↑r * x).arg = x.arg
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>x : ℂ<GOAL>(x * ↑r).arg = x.arg
<VAR>x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>x.arg = y.arg ↔ ↑(Complex.abs y) / ↑(Complex.abs x) * x = y
<VAR>x : ℂ<GOAL>Real.tan x.arg = x.im / x.re
<VAR>x : ℝ<VAR>hx : 0 ≤ x<GOAL>(↑x).arg = 0
<VAR>n : ℕ<GOAL>(↑n).arg = 0
<VAR>n : ℕ<VAR>n.AtLeastTwo<GOAL>(OfNat.ofNat n).arg = 0
<VAR>z : ℂ<GOAL>z.arg = 0 ↔ 0 ≤ z.re ∧ z.im = 0
<VAR>z : ℂ<GOAL>z.arg = 0 ↔ 0 ≤ z
<VAR>z : ℂ<GOAL>z.arg = π ↔ z.re < 0 ∧ z.im = 0
<VAR>z : ℂ<GOAL>z.arg = π ↔ z < 0
<VAR>z : ℂ<GOAL>z.arg < π ↔ 0 ≤ z.re ∨ z.im ≠ 0
<VAR>x : ℝ<VAR>hx : x < 0<GOAL>(↑x).arg = π
<VAR>z : ℂ<GOAL>z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im
<VAR>z : ℂ<GOAL>z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0
<VAR>x : ℂ<VAR>hx : 0 ≤ x.re<GOAL>x.arg = Real.arcsin (x.im / Complex.abs x)
<VAR>x : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : 0 ≤ x.im<GOAL>x.arg = Real.arcsin ((-x).im / Complex.abs x) + π
<VAR>x : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : x.im < 0<GOAL>x.arg = Real.arcsin ((-x).im / Complex.abs x) - π
<VAR>z : ℂ<VAR>h₁ : 0 ≤ z.im<VAR>h₂ : z ≠ 0<GOAL>z.arg = Real.arccos (z.re / Complex.abs z)
<VAR>z : ℂ<VAR>hz : 0 < z.im<GOAL>z.arg = Real.arccos (z.re / Complex.abs z)
<VAR>z : ℂ<VAR>hz : z.im < 0<GOAL>z.arg = -Real.arccos (z.re / Complex.abs z)
<VAR>x : ℂ<GOAL>((starRingEnd ℂ) x).arg = if x.arg = π then π else -x.arg
<VAR>x : ℂ<GOAL>x⁻¹.arg = if x.arg = π then π else -x.arg
<VAR>x : ℂ<GOAL>|x⁻¹.arg| = |x.arg|
<VAR>x : ℂ<GOAL>Complex.abs x = 1 ↔ ∃ θ ∈ Set.Ioc (-π) π, Complex.exp (↑θ * Complex.I) = x
<GOAL>(fun θ => Complex.exp (↑θ * Complex.I)) '' Set.Ioc (-π) π = Metric.sphere 0 1
<VAR>z : ℂ<GOAL>z.arg ≤ π / 2 ↔ 0 ≤ z.re ∨ z.im < 0
<VAR>z : ℂ<GOAL>-(π / 2) ≤ z.arg ↔ 0 ≤ z.re ∨ 0 ≤ z.im
<VAR>z : ℂ<GOAL>-(π / 2) < z.arg ↔ 0 < z.re ∨ 0 ≤ z.im
<VAR>z : ℂ<GOAL>z.arg < π / 2 ↔ 0 < z.re ∨ z.im < 0 ∨ z = 0
<VAR>z : ℂ<GOAL>|z.arg| ≤ π / 2 ↔ 0 ≤ z.re
<VAR>z : ℂ<GOAL>|z.arg| < π / 2 ↔ 0 < z.re ∨ z = 0
<VAR>x : ℂ<GOAL>↑((starRingEnd ℂ) x).arg = -↑x.arg
<VAR>x : ℂ<GOAL>↑x⁻¹.arg = -↑x.arg
<VAR>x : ℂ<VAR>hi : 0 < x.im<GOAL>(-x).arg = x.arg - π
<VAR>x : ℂ<VAR>hi : x.im < 0<GOAL>(-x).arg = x.arg + π
<VAR>x : ℂ<GOAL>(-x).arg = x.arg - π ↔ 0 < x.im ∨ x.im = 0 ∧ x.re < 0
<VAR>x : ℂ<GOAL>(-x).arg = x.arg + π ↔ x.im < 0 ∨ x.im = 0 ∧ 0 < x.re
<VAR>x : ℂ<VAR>hx : x ≠ 0<GOAL>↑(-x).arg = ↑x.arg + ↑π
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>(↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg = toIocMod Real.two_pi_pos (-π) θ
<VAR>θ : ℝ<GOAL>(Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg = toIocMod Real.two_pi_pos (-π) θ
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : ℝ<GOAL>(↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
<VAR>θ : ℝ<GOAL>(Complex.cos ↑θ + Complex.sin ↑θ * Complex.I).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
<VAR>r : ℝ<VAR>hr : 0 < r<VAR>θ : Real.Angle<GOAL>↑(↑r * (↑θ.cos + ↑θ.sin * Complex.I)).arg = θ
<VAR>θ : Real.Angle<GOAL>↑(↑θ.cos + ↑θ.sin * Complex.I).arg = θ
<VAR>x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑(x * y).arg = ↑x.arg + ↑y.arg
<VAR>x y : ℂ<VAR>hx : x ≠ 0<VAR>hy : y ≠ 0<GOAL>↑(x / y).arg = ↑x.arg - ↑y.arg
<VAR>z : ℂ<GOAL>(↑z.arg).toReal = z.arg
<VAR>z : ℂ<VAR>θ : Real.Angle<GOAL>↑z.arg = θ ↔ z.arg = θ.toReal
<VAR>x y : ℂ<GOAL>↑x.arg = ↑y.arg ↔ x.arg = y.arg
<VAR>x y : ℂ<VAR>hx₀ : x ≠ 0<VAR>hy₀ : y ≠ 0<GOAL>(x * y).arg = x.arg + y.arg ↔ x.arg + y.arg ∈ Set.Ioc (-π) π
<VAR>z : ℂ<GOAL>z ∈ Complex.slitPlane ↔ z.arg ≠ π ∧ z ≠ 0
<VAR>z : ℂ<VAR>hz : z ∈ Complex.slitPlane<GOAL>z.arg ≠ π
<VAR>x : ℂ<VAR>hx : 0 < x.re<GOAL>Complex.arg =ᶠ[𝓝 x] fun x => Real.arcsin (x.im / Complex.abs x)
<VAR>x : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : 0 < x.im<GOAL>Complex.arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / Complex.abs x) + π
<VAR>x : ℂ<VAR>hx_re : x.re < 0<VAR>hx_im : x.im < 0<GOAL>Complex.arg =ᶠ[𝓝 x] fun x => Real.arcsin ((-x).im / Complex.abs x) - π
<VAR>z : ℂ<VAR>hz : 0 < z.im<GOAL>Complex.arg =ᶠ[𝓝 z] fun x => Real.arccos (x.re / Complex.abs x)
<VAR>z : ℂ<VAR>hz : z.im < 0<GOAL>Complex.arg =ᶠ[𝓝 z] fun x => -Real.arccos (x.re / Complex.abs x)
<VAR>x : ℂ<VAR>h : x ∈ Complex.slitPlane<GOAL>ContinuousAt Complex.arg x
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Filter.Tendsto Complex.arg (𝓝[{z | z.im < 0}] z) (𝓝 (-π))
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>ContinuousWithinAt Complex.arg {z | 0 ≤ z.im} z
<VAR>z : ℂ<VAR>hre : z.re < 0<VAR>him : z.im = 0<GOAL>Filter.Tendsto Complex.arg (𝓝[{z | 0 ≤ z.im}] z) (𝓝 π)
<VAR>x : ℂ<VAR>h : x ≠ 0<GOAL>ContinuousAt (Real.Angle.coe ∘ Complex.arg) x
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : M<VAR>self : IsLprojection X P<GOAL>IsIdempotentElem P
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : M<VAR>self : IsLprojection X P<VAR>x : X<GOAL>‖x‖ = ‖P • x‖ + ‖(1 - P) • x‖
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : M<VAR>self : IsMprojection X P<GOAL>IsIdempotentElem P
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : M<VAR>self : IsMprojection X P<VAR>x : X<GOAL>‖x‖ = max ‖P • x‖ ‖(1 - P) • x‖
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : M<VAR>h : IsLprojection X P<GOAL>IsLprojection X (1 - P)
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : M<GOAL>IsLprojection X P ↔ IsLprojection X (1 - P)
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>Commute P Q
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>IsLprojection X (P * Q)
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q : M<VAR>h₁ : IsLprojection X P<VAR>h₂ : IsLprojection X Q<GOAL>IsLprojection X (P + Q - P * Q)
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : { P // IsLprojection X P }<GOAL>↑Pᶜ = 1 - ↑P
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q : { P // IsLprojection X P }<GOAL>↑(P ⊓ Q) = ↑P * ↑Q
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q : { P // IsLprojection X P }<GOAL>↑(P ⊔ Q) = ↑P + ↑Q - ↑P * ↑Q
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q : { P // IsLprojection X P }<GOAL>↑(P \ Q) = ↑P * (1 - ↑Q)
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q : { P // IsLprojection X P }<GOAL>P ≤ Q ↔ ↑P = ↑(P ⊓ Q)
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<GOAL>↑0 = 0
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<GOAL>↑1 = 1
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<GOAL>↑⊥ = 0
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<GOAL>↑⊤ = 1
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : { P // IsLprojection X P }<VAR>Q : M<GOAL>↑Pᶜ * Q = Q - ↑P * Q
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>P : { P // IsLprojection X P }<GOAL>↑P * ↑Pᶜ = 0
<VAR>X : Type u_1<VAR>NormedAddCommGroup X<VAR>M : Type u_2<VAR>Ring M<VAR>Module M X<VAR>FaithfulSMul M X<VAR>P Q R : { P // IsLprojection X P }<GOAL>(↑P + ↑Pᶜ * ↑R) * (↑P + ↑Q * ↑R * ↑Pᶜ) = ↑P + ↑Q * ↑R * ↑Pᶜ
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>x y : PE<VAR>e : PE ≃ᵢ PE<GOAL>e x = x → e y = y → e (midpoint ℝ x y) = midpoint ℝ x y
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>MetricSpace PF<VAR>NormedAddTorsor F PF<VAR>f : PE ≃ᵢ PF<VAR>x y : PE<GOAL>f (midpoint ℝ x y) = midpoint ℝ (f x) (f y)
<VAR>E : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E ≃ᵢ F<VAR>h0 : f 0 = 0<GOAL>⇑(f.toRealLinearIsometryEquivOfMapZero h0) = ⇑f
<VAR>E : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E ≃ᵢ F<VAR>h0 : f 0 = 0<GOAL>⇑(f.toRealLinearIsometryEquivOfMapZero h0).symm = ⇑f.symm
<VAR>E : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E ≃ᵢ F<VAR>x : E<GOAL>f.toRealLinearIsometryEquiv x = f x - f 0
<VAR>E : Type u_1<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>f : E ≃ᵢ F<VAR>y : F<GOAL>f.toRealLinearIsometryEquiv.symm y = f.symm (y + f 0)
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>MetricSpace PF<VAR>NormedAddTorsor F PF<VAR>f : PE ≃ᵢ PF<GOAL>⇑f.toRealAffineIsometryEquiv = ⇑f
<VAR>E : Type u_1<VAR>PE : Type u_2<VAR>F : Type u_3<VAR>PF : Type u_4<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>MetricSpace PE<VAR>NormedAddTorsor E PE<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>MetricSpace PF<VAR>NormedAddTorsor F PF<VAR>f : PE ≃ᵢ PF<GOAL>f.toRealAffineIsometryEquiv.toIsometryEquiv = f
<VAR>p : ℂ × ℂ<VAR>hp : p.1 ∈ Complex.slitPlane<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * Complex.log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p
<VAR>x y : ℂ<VAR>hp : x ∈ Complex.slitPlane<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((y * x ^ (y - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (x ^ y * Complex.log x) • ContinuousLinearMap.snd ℂ ℂ ℂ) (x, y)
<VAR>x y : ℂ<VAR>h : x ≠ 0 ∨ y ≠ 0<GOAL>HasStrictDerivAt (fun y => x ^ y) (x ^ y * Complex.log x) y
<VAR>p : ℂ × ℂ<VAR>hp : p.1 ∈ Complex.slitPlane<GOAL>HasFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℂ ℂ ℂ + (p.1 ^ p.2 * Complex.log p.1) • ContinuousLinearMap.snd ℂ ℂ ℂ) p
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>f' g' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') 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>h0 : c ≠ 0 ∨ f x ≠ 0<GOAL>HasStrictFDerivAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>f' g' : E →L[ℂ] ℂ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>hg : HasFDerivAt g g' x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') 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>h0 : c ≠ 0 ∨ f x ≠ 0<GOAL>HasFDerivAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>f' g' : E →L[ℂ] ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt g g' s x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Complex.log (f x)) • g') s x
<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>h0 : c ≠ 0 ∨ f x ≠ 0<GOAL>HasFDerivWithinAt (fun x => c ^ f x) ((c ^ f x * Complex.log c) • f') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>x : E<VAR>hf : DifferentiableAt ℂ f x<VAR>hg : DifferentiableAt ℂ g x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>DifferentiableAt ℂ (fun x => f x ^ g x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>c : ℂ<VAR>hf : DifferentiableAt ℂ f x<VAR>h0 : c ≠ 0 ∨ f x ≠ 0<GOAL>DifferentiableAt ℂ (fun x => c ^ f x) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>hg : DifferentiableWithinAt ℂ g s x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>DifferentiableWithinAt ℂ (fun x => f x ^ g x) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>x : E<VAR>s : Set E<VAR>c : ℂ<VAR>hf : DifferentiableWithinAt ℂ f s x<VAR>h0 : c ≠ 0 ∨ f x ≠ 0<GOAL>DifferentiableWithinAt ℂ (fun x => c ^ f x) s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>s : Set E<VAR>hf : DifferentiableOn ℂ f s<VAR>hg : DifferentiableOn ℂ g s<VAR>h0 : Set.MapsTo f s Complex.slitPlane<GOAL>DifferentiableOn ℂ (fun x => f x ^ g x) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>s : Set E<VAR>c : ℂ<VAR>hf : DifferentiableOn ℂ f s<VAR>h0 : c ≠ 0 ∨ ∀ x ∈ s, f x ≠ 0<GOAL>DifferentiableOn ℂ (fun x => c ^ f x) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f g : E → ℂ<VAR>hf : Differentiable ℂ f<VAR>hg : Differentiable ℂ g<VAR>h0 : ∀ (x : E), f x ∈ Complex.slitPlane<GOAL>Differentiable ℂ fun x => f x ^ g x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℂ E<VAR>f : E → ℂ<VAR>c : ℂ<VAR>hf : Differentiable ℂ f<VAR>h0 : c ≠ 0 ∨ ∀ (x : E), f x ≠ 0<GOAL>Differentiable ℂ fun x => c ^ f x
<VAR>f g : ℂ → ℂ<VAR>f' g' x : ℂ<GOAL>((g x * f x ^ (g x - 1)) • ContinuousLinearMap.smulRight 1 f' + (f x ^ g x * Complex.log (f x)) • ContinuousLinearMap.smulRight 1 g') 1 = g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g'
<VAR>f g : ℂ → ℂ<VAR>f' g' x : ℂ<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasStrictDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
<VAR>f : ℂ → ℂ<VAR>f' x c : ℂ<VAR>hf : HasStrictDerivAt f f' x<VAR>h : c ≠ 0 ∨ f x ≠ 0<GOAL>HasStrictDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x
<VAR>x c : ℂ<VAR>h : x ∈ Complex.slitPlane<GOAL>HasStrictDerivAt (fun z => z ^ c) (c * x ^ (c - 1)) x
<VAR>f : ℂ → ℂ<VAR>f' x c : ℂ<VAR>hf : HasStrictDerivAt f f' x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasStrictDerivAt (fun x => f x ^ c) (c * f x ^ (c - 1) * f') x
<VAR>f g : ℂ → ℂ<VAR>f' g' x : ℂ<VAR>hf : HasDerivAt f f' x<VAR>hg : HasDerivAt g g' x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasDerivAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') x
<VAR>f : ℂ → ℂ<VAR>f' x c : ℂ<VAR>hf : HasDerivAt f f' x<VAR>h0 : c ≠ 0 ∨ f x ≠ 0<GOAL>HasDerivAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') x
<VAR>f : ℂ → ℂ<VAR>f' x c : ℂ<VAR>hf : HasDerivAt f f' x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasDerivAt (fun x => f x ^ c) (c * f x ^ (c - 1) * f') x
<VAR>f g : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' g' x : ℂ<VAR>hf : HasDerivWithinAt f f' s x<VAR>hg : HasDerivWithinAt g g' s x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasDerivWithinAt (fun x => f x ^ g x) (g x * f x ^ (g x - 1) * f' + f x ^ g x * Complex.log (f x) * g') s x
<VAR>f : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' x c : ℂ<VAR>hf : HasDerivWithinAt f f' s x<VAR>h0 : c ≠ 0 ∨ f x ≠ 0<GOAL>HasDerivWithinAt (fun x => c ^ f x) (c ^ f x * Complex.log c * f') s x
<VAR>f : ℂ → ℂ<VAR>s : Set ℂ<VAR>f' x c : ℂ<VAR>hf : HasDerivWithinAt f f' s x<VAR>h0 : f x ∈ Complex.slitPlane<GOAL>HasDerivWithinAt (fun x => f x ^ c) (c * f x ^ (c - 1) * f') s x
<VAR>x : ℝ<VAR>hx : x ≠ 0<VAR>r : ℂ<VAR>hr : r ≠ -1<GOAL>HasDerivAt (fun y => ↑y ^ (r + 1) / (r + 1)) (↑x ^ r) x
<VAR>p : ℝ × ℝ<VAR>hp : 0 < p.1<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * Real.log p.1) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
<VAR>p : ℝ × ℝ<VAR>hp : p.1 < 0<GOAL>HasStrictFDerivAt (fun x => x.1 ^ x.2) ((p.2 * p.1 ^ (p.2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ + (p.1 ^ p.2 * Real.log p.1 - rexp (Real.log p.1 * p.2) * Real.sin (p.2 * π) * π) • ContinuousLinearMap.snd ℝ ℝ ℝ) p
<VAR>p : ℝ × ℝ<VAR>hp : p.1 ≠ 0<VAR>n : ℕ∞<GOAL>ContDiffAt ℝ n (fun p => p.1 ^ p.2) p
<VAR>p : ℝ × ℝ<VAR>hp : p.1 ≠ 0<GOAL>DifferentiableAt ℝ (fun p => p.1 ^ p.2) p
<VAR>x : ℝ<VAR>f g : ℝ → ℝ<VAR>f' g' : ℝ<VAR>hf : HasStrictDerivAt f f' x<VAR>hg : HasStrictDerivAt g g' x<VAR>h : 0 < f x<GOAL>HasStrictDerivAt (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>x : ℝ<VAR>hx : x ≠ 0<VAR>p : ℝ<GOAL>HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>a : ℝ<VAR>ha : 0 < a<VAR>x : ℝ<GOAL>HasStrictDerivAt (fun x => a ^ x) (a ^ x * Real.log a) x
<VAR>p : ℝ<VAR>x : ℝ<VAR>hx : x ≠ 0<GOAL>DifferentiableAt ℝ (fun x => x ^ p) x
<VAR>p : ℝ<GOAL>DifferentiableOn ℝ (fun x => x ^ p) {0}ᶜ
<VAR>a x : ℝ<VAR>ha : a < 0<GOAL>HasStrictDerivAt (fun x => a ^ x) (a ^ x * Real.log a - rexp (Real.log a * x) * Real.sin (x * π) * π) x
<VAR>x p : ℝ<VAR>h : x ≠ 0 ∨ 1 ≤ p<GOAL>HasDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>p : ℝ<VAR>hp : 1 ≤ p<GOAL>Differentiable ℝ fun x => x ^ p
<VAR>x p : ℝ<VAR>h : x ≠ 0 ∨ 1 ≤ p<GOAL>deriv (fun x => x ^ p) x = p * x ^ (p - 1)
<VAR>p : ℝ<VAR>h : 1 ≤ p<GOAL>(deriv fun x => x ^ p) = fun x => p * x ^ (p - 1)
<VAR>x p : ℝ<VAR>n : ℕ∞<VAR>h : x ≠ 0<GOAL>ContDiffAt ℝ n (fun x => x ^ p) x
<VAR>p : ℝ<VAR>n : ℕ<VAR>h : ↑n ≤ p<GOAL>ContDiff ℝ ↑n fun x => x ^ p
<VAR>x p : ℝ<VAR>n : ℕ<VAR>h : ↑n ≤ p<GOAL>ContDiffAt ℝ (↑n) (fun x => x ^ p) x
<VAR>x p : ℝ<VAR>n : ℕ<VAR>h : x ≠ 0 ∨ ↑n ≤ p<GOAL>ContDiffAt ℝ (↑n) (fun x => x ^ p) x
<VAR>x p : ℝ<VAR>hx : x ≠ 0 ∨ 1 ≤ p<GOAL>HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>f' g' : E →L[ℝ] ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : HasFDerivWithinAt f f' s x<VAR>hg : HasFDerivWithinAt g g' s x<VAR>h : 0 < f x<GOAL>HasFDerivWithinAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') s x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>f' g' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasFDerivAt f f' x<VAR>hg : HasFDerivAt g g' x<VAR>h : 0 < f x<GOAL>HasFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>f' g' : E →L[ℝ] ℝ<VAR>x : E<VAR>hf : HasStrictFDerivAt f f' x<VAR>hg : HasStrictFDerivAt g g' x<VAR>h : 0 < f x<GOAL>HasStrictFDerivAt (fun x => f x ^ g x) ((g x * f x ^ (g x - 1)) • f' + (f x ^ g x * Real.log (f x)) • g') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>x : E<VAR>s : Set E<VAR>hf : DifferentiableWithinAt ℝ f s x<VAR>hg : DifferentiableWithinAt ℝ g s x<VAR>h : f x ≠ 0<GOAL>DifferentiableWithinAt ℝ (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>hf : DifferentiableAt ℝ f x<VAR>hg : DifferentiableAt ℝ g x<VAR>h : f x ≠ 0<GOAL>DifferentiableAt ℝ (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>hf : DifferentiableOn ℝ f s<VAR>hg : DifferentiableOn ℝ g s<VAR>h : ∀ x ∈ s, f x ≠ 0<GOAL>DifferentiableOn ℝ (fun x => f x ^ g x) s
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f g : E → ℝ<VAR>hf : Differentiable ℝ f<VAR>hg : Differentiable ℝ g<VAR>h : ∀ (x : E), f x ≠ 0<GOAL>Differentiable ℝ fun x => f x ^ g x
<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>p : ℝ<VAR>hf : HasFDerivWithinAt f f' s x<VAR>h : f x ≠ 0 ∨ 1 ≤ p<GOAL>HasFDerivWithinAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • 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>p : ℝ<VAR>hf : HasFDerivAt f f' x<VAR>h : f x ≠ 0 ∨ 1 ≤ p<GOAL>HasFDerivAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') x
<VAR>E : Type u_1<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>f : E → ℝ<VAR>f' : E →L[ℝ] ℝ<VAR>x : E<VAR>p : ℝ<VAR>hf : HasStrictFDerivAt f f' x<VAR>h : f x ≠ 0 ∨ 1 ≤ p<GOAL>HasStrictFDerivAt (fun x => f x ^ p) ((p * f x ^ (p - 1)) • f') x