ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>𝕜₂ : Type u_2<VAR>𝕜₃ : Type u_3<VAR>F : Type u_6<VAR>G : Type u_8<VAR>NormedAddCommGroup F<VAR>NormedAddCommGroup G<VAR>NontriviallyNormedField 𝕜₂<VAR>NontriviallyNormedField 𝕜₃<VAR>NormedSpace 𝕜₂ F<VAR>NormedSpace 𝕜₃ G<VAR>σ₂₃ : 𝕜₂ →+* 𝕜₃<VAR>𝕜₂' : Type u_11<VAR>NontriviallyNormedField 𝕜₂'<VAR>F' : Type u_12<VAR>NormedAddCommGroup F'<VAR>NormedSpace 𝕜₂' F'<VAR>σ₂' : 𝕜₂' →+* 𝕜₂<VAR>σ₂'' : 𝕜₂ →+* 𝕜₂'<VAR>σ₂₃' : 𝕜₂' →+* 𝕜₃<VAR>RingHomInvPair σ₂' σ₂''<VAR>RingHomInvPair σ₂'' σ₂'<VAR>RingHomCompTriple σ₂' σ₂₃ σ₂₃'<VAR>RingHomCompTriple σ₂'' σ₂₃' σ₂₃<VAR>RingHomIsometric σ₂₃<VAR>RingHomIsometric σ₂'<VAR>RingHomIsometric σ₂''<VAR>RingHomIsometric σ₂₃'<VAR>f : F →SL[σ₂₃] G<VAR>g : F' ≃ₛₗᵢ[σ₂'] F<GOAL>‖f.comp g.toLinearIsometry.toContinuousLinearMap‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>c : E →L[𝕜] 𝕜<VAR>f : Fₗ<GOAL>‖c.smulRight f‖ = ‖c‖ * ‖f‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>c : E →L[𝕜] 𝕜<VAR>f : Fₗ<GOAL>‖c.smulRight f‖₊ = ‖c‖₊ * ‖f‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>c : E →L[𝕜] 𝕜<VAR>f : Fₗ<GOAL>‖((ContinuousLinearMap.smulRightL 𝕜 E Fₗ) c) f‖ = ‖c‖ * ‖f‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<VAR>c : E →L[𝕜] 𝕜<VAR>Nontrivial Fₗ<GOAL>‖(ContinuousLinearMap.smulRightL 𝕜 E Fₗ) c‖ = ‖c‖
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>Fₗ : Type u_7<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup Fₗ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 Fₗ<GOAL>‖ContinuousLinearMap.smulRightL 𝕜 E Fₗ‖ ≤ 1
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>K : Submodule 𝕜 E<VAR>Nontrivial ↥K<GOAL>‖K.subtypeL‖ = 1
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>e : E ≃SL[σ₁₂] F<GOAL>AntilipschitzWith ‖↑e.symm‖₊ ⇑e
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>RingHomIsometric σ₁₂<VAR>Nontrivial E<VAR>e : E ≃SL[σ₁₂] F<GOAL>1 ≤ ‖↑e‖ * ‖↑e.symm‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>RingHomIsometric σ₁₂<VAR>Nontrivial E<VAR>e : E ≃SL[σ₁₂] F<GOAL>0 < ‖↑e‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>RingHomIsometric σ₁₂<VAR>Nontrivial E<VAR>e : E ≃SL[σ₁₂] F<GOAL>0 < ‖↑e.symm‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>RingHomIsometric σ₁₂<VAR>Nontrivial E<VAR>e : E ≃SL[σ₁₂] F<GOAL>0 < ‖↑e.symm‖₊
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>RingHomIsometric σ₁₂<VAR>e : E ≃SL[σ₁₂] F<GOAL>Subsingleton E ∨ 0 < ‖↑e.symm‖
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedAddCommGroup F<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>σ₂₁ : 𝕜₂ →+* 𝕜<VAR>RingHomInvPair σ₁₂ σ₂₁<VAR>RingHomInvPair σ₂₁ σ₁₂<VAR>RingHomIsometric σ₂₁<VAR>RingHomIsometric σ₁₂<VAR>e : E ≃SL[σ₁₂] F<GOAL>Subsingleton E ∨ 0 < ‖↑e.symm‖₊
<VAR>𝕜 : Type u_1<VAR>E : Type u_4<VAR>NormedAddCommGroup E<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<GOAL>‖ContinuousLinearEquiv.coord 𝕜 x h‖ = ‖x‖⁻¹
<VAR>𝕜 : Type u_1<VAR>𝕜₂ : Type u_2<VAR>E : Type u_4<VAR>F : Type u_6<VAR>ι : Type u_11<VAR>NontriviallyNormedField 𝕜<VAR>NontriviallyNormedField 𝕜₂<VAR>σ₁₂ : 𝕜 →+* 𝕜₂<VAR>RingHomIsometric σ₁₂<VAR>SeminormedAddCommGroup E<VAR>SeminormedAddCommGroup F<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜₂ F<VAR>f : ι → E →SL[σ₁₂] F<GOAL>[EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C, ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun x => ‖f x‖), ⨆ i, ↑‖f i‖₊ < ⊤].TFAE
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<VAR>r : ℝ<VAR>hr : r < 1<GOAL>∃ x₀ ∉ F, ∀ y ∈ F, r * ‖x₀‖ ≤ ‖x₀ - y‖
<VAR>𝕜 : Type u_1<VAR>NormedField 𝕜<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>c : 𝕜<VAR>hc : 1 < ‖c‖<VAR>R : ℝ<VAR>hR : ‖c‖ < R<VAR>F : Subspace 𝕜 E<VAR>hFc : IsClosed ↑F<VAR>hF : ∃ x, x ∉ F<GOAL>∃ x₀, ‖x₀‖ ≤ R ∧ ∀ y ∈ F, 1 ≤ ‖x₀ - y‖
<VAR>F : Type u_3<VAR>SeminormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>x : F<VAR>s : Set F<VAR>hx : x ∈ s<GOAL>Metric.closedBall x (Metric.infDist x sᶜ) ⊆ closure s
<VAR>R : Type u_1<VAR>AddCommMonoid R<VAR>m : ℕ<VAR>NeZero m<VAR>f : ℕ → R<GOAL>f = ∑ a : ZMod m, {n | ↑n = a}.indicator f
<VAR>R : Type u_1<VAR>AddCommGroup R<VAR>TopologicalSpace R<VAR>TopologicalAddGroup R<VAR>m : ℕ<VAR>hm : NeZero m<VAR>k : ℕ<VAR>f : ℕ → R<GOAL>Summable ({n | ↑n = ↑k}.indicator f) ↔ Summable fun n => f (m * n + k)
<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>n : ℕ<VAR>hn : f n < 0<GOAL>¬Summable f
<VAR>m : ℕ<VAR>hm : NeZero m<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>n : ℕ<VAR>hn : f n < 0<VAR>k : ZMod m<GOAL>¬Summable ({n | ↑n = k}.indicator f)
<VAR>m : ℕ<VAR>NeZero m<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>k : ZMod m<VAR>l : ZMod m<VAR>hs : Summable ({n | ↑n = k}.indicator f)<GOAL>Summable ({n | ↑n = l}.indicator f)
<VAR>m : ℕ<VAR>NeZero m<VAR>f : ℕ → ℝ<VAR>hf : Antitone f<VAR>k : ZMod m<GOAL>Summable ({n | ↑n = k}.indicator f) ↔ Summable f
<VAR>a b : ℝ<VAR>n : ℕ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>IntervalIntegrable (fun x => x ^ n) μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>n : ℤ<VAR>h : 0 ≤ n ∨ 0 ∉ [[a, b]]<GOAL>IntervalIntegrable (fun x => x ^ n) μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>r : ℝ<VAR>h : 0 ≤ r ∨ 0 ∉ [[a, b]]<GOAL>IntervalIntegrable (fun x => x ^ r) μ a b
<VAR>a b r : ℝ<VAR>h : -1 < r<GOAL>IntervalIntegrable (fun x => x ^ r) MeasureTheory.volume a b
<VAR>s t : ℝ<VAR>ht : 0 < t<GOAL>MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>r : ℂ<VAR>h : 0 ≤ r.re ∨ 0 ∉ [[a, b]]<GOAL>IntervalIntegrable (fun x => ↑x ^ r) μ a b
<VAR>a b : ℝ<VAR>r : ℂ<VAR>h : -1 < r.re<GOAL>IntervalIntegrable (fun x => ↑x ^ r) MeasureTheory.volume a b
<VAR>s : ℂ<VAR>t : ℝ<VAR>ht : 0 < t<GOAL>MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s.re
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>IntervalIntegrable (fun x => x) μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>c : ℝ<GOAL>IntervalIntegrable (fun x => c) μ a b
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>h : ∀ x ∈ [[a, b]], f x ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<GOAL>IntervalIntegrable (fun x => 1 / f x) μ a b
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>h : ∀ x ∈ [[a, b]], f x ≠ 0<VAR>hf : ContinuousOn f [[a, b]]<GOAL>IntervalIntegrable (fun x => (f x)⁻¹) μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>IntervalIntegrable rexp μ a b
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>hf : ContinuousOn f [[a, b]]<VAR>h : ∀ x ∈ [[a, b]], f x ≠ 0<GOAL>IntervalIntegrable (fun x => Real.log (f x)) μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<VAR>h : 0 ∉ [[a, b]]<GOAL>IntervalIntegrable Real.log μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>IntervalIntegrable Real.sin μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>IntervalIntegrable Real.cos μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>IntervalIntegrable (fun x => 1 / (1 + x ^ 2)) μ a b
<VAR>a b : ℝ<VAR>μ : MeasureTheory.Measure ℝ<VAR>MeasureTheory.IsLocallyFiniteMeasure μ<GOAL>IntervalIntegrable (fun x => (1 + x ^ 2)⁻¹) μ a b
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c : ℝ<GOAL>c * ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c : ℝ<GOAL>c * ∫ (x : ℝ) in a..b, f (c * x) = ∫ (x : ℝ) in c * a..c * b, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c : ℝ<GOAL>c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c) = ∫ (x : ℝ) in a / c..b / c, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c * ∫ (x : ℝ) in a..b, f (c * x + d) = ∫ (x : ℝ) in c * a + d..c * b + d, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c * ∫ (x : ℝ) in a..b, f (d + c * x) = ∫ (x : ℝ) in d + c * a..d + c * b, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c + d) = ∫ (x : ℝ) in a / c + d..b / c + d, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c⁻¹ * ∫ (x : ℝ) in a..b, f (d + x / c) = ∫ (x : ℝ) in d + a / c..d + b / c, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c * ∫ (x : ℝ) in a..b, f (c * x - d) = ∫ (x : ℝ) in c * a - d..c * b - d, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c * ∫ (x : ℝ) in a..b, f (d - c * x) = ∫ (x : ℝ) in d - c * b..d - c * a, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c⁻¹ * ∫ (x : ℝ) in a..b, f (x / c - d) = ∫ (x : ℝ) in a / c - d..b / c - d, f x
<VAR>a b : ℝ<VAR>f : ℝ → ℝ<VAR>c d : ℝ<GOAL>c⁻¹ * ∫ (x : ℝ) in a..b, f (d - x / c) = ∫ (x : ℝ) in d - b / c..d - a / c, f x
<VAR>a b : ℝ<VAR>r : ℂ<VAR>h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, ↑x ^ r = (↑b ^ (r + 1) - ↑a ^ (r + 1)) / (r + 1)
<VAR>a b r : ℝ<VAR>h : -1 < r ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, x ^ r = (b ^ (r + 1) - a ^ (r + 1)) / (r + 1)
<VAR>a b : ℝ<VAR>n : ℤ<VAR>h : 0 ≤ n ∨ n ≠ -1 ∧ 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1)
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, x = (b ^ 2 - a ^ 2) / 2
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, 1 = b - a
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..a + 1, b = b
<VAR>a b : ℝ<VAR>h : 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
<VAR>a b : ℝ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>∫ (x : ℝ) in a..b, x⁻¹ = Real.log (b / a)
<VAR>a b : ℝ<VAR>h : 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
<VAR>a b : ℝ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, rexp x = rexp b - rexp a
<VAR>a b : ℝ<VAR>c : ℂ<VAR>hc : c ≠ 0<GOAL>∫ (x : ℝ) in a..b, Complex.exp (c * ↑x) = (Complex.exp (c * ↑b) - Complex.exp (c * ↑a)) / c
<VAR>a b : ℝ<VAR>h : 0 ∉ [[a, b]]<GOAL>∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
<VAR>a b : ℝ<VAR>ha : 0 < a<VAR>hb : 0 < b<GOAL>∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
<VAR>a b : ℝ<VAR>ha : a < 0<VAR>hb : b < 0<GOAL>∫ (x : ℝ) in a..b, Real.log x = b * Real.log b - a * Real.log a - b + a
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x = Real.cos a - Real.cos b
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.cos x = Real.sin b - Real.sin a
<VAR>z : ℂ<VAR>hz : z ≠ 0<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Complex.cos (z * ↑x) = Complex.sin (z * ↑b) / z - Complex.sin (z * ↑a) / z
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.cos x ^ 2 - Real.sin x ^ 2 = Real.sin b * Real.cos b - Real.sin a * Real.cos a
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = Real.arctan b - Real.arctan a
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = Real.arctan b - Real.arctan a
<VAR>a b : ℝ<VAR>t : ℂ<VAR>ht : t ≠ -1<GOAL>∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t = (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))
<VAR>a b t : ℝ<VAR>ht : t ≠ -1<GOAL>∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ (n + 2) = (Real.sin a ^ (n + 1) * Real.cos a - Real.sin b ^ (n + 1) * Real.cos b + (↑n + 1) * ∫ (x : ℝ) in a..b, Real.sin x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, Real.sin x ^ (n + 2)
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ (n + 2) = (Real.sin a ^ (n + 1) * Real.cos a - Real.sin b ^ (n + 1) * Real.cos b) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, Real.sin x ^ n
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ 2 = (Real.sin a * Real.cos a - Real.sin b * Real.cos b + b - a) / 2
<VAR>n : ℕ<GOAL>∫ (x : ℝ) in 0 ..π, Real.sin x ^ (2 * n + 1) = 2 * ∏ i ∈ Finset.range n, (2 * ↑i + 2) / (2 * ↑i + 3)
<VAR>n : ℕ<GOAL>∫ (x : ℝ) in 0 ..π, Real.sin x ^ (2 * n) = π * ∏ i ∈ Finset.range n, (2 * ↑i + 1) / (2 * ↑i + 2)
<VAR>n : ℕ<GOAL>0 < ∫ (x : ℝ) in 0 ..π, Real.sin x ^ n
<VAR>n : ℕ<GOAL>∫ (x : ℝ) in 0 ..π, Real.sin x ^ (n + 1) ≤ ∫ (x : ℝ) in 0 ..π, Real.sin x ^ n
<GOAL>Antitone fun n => ∫ (x : ℝ) in 0 ..π, Real.sin x ^ n
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, Real.cos x ^ (n + 2) = (Real.cos b ^ (n + 1) * Real.sin b - Real.cos a ^ (n + 1) * Real.sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, Real.cos x ^ n) - (↑n + 1) * ∫ (x : ℝ) in a..b, Real.cos x ^ (n + 2)
<VAR>a b : ℝ<VAR>n : ℕ<GOAL>∫ (x : ℝ) in a..b, Real.cos x ^ (n + 2) = (Real.cos b ^ (n + 1) * Real.sin b - Real.cos a ^ (n + 1) * Real.sin a) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, Real.cos x ^ n
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.cos x ^ 2 = (Real.cos b * Real.sin b - Real.cos a * Real.sin a + b - a) / 2
<VAR>a b : ℝ<VAR>m n : ℕ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ m * Real.cos x ^ (2 * n + 1) = ∫ (u : ℝ) in Real.sin a..Real.sin b, u ^ m * (1 - u ^ 2) ^ n
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x * Real.cos x = (Real.sin b ^ 2 - Real.sin a ^ 2) / 2
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ 2 * Real.cos x = (Real.sin b ^ 3 - Real.sin a ^ 3) / 3
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.cos x ^ 3 = Real.sin b - Real.sin a - (Real.sin b ^ 3 - Real.sin a ^ 3) / 3
<VAR>a b : ℝ<VAR>m n : ℕ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ (2 * m + 1) * Real.cos x ^ n = ∫ (u : ℝ) in Real.cos b..Real.cos a, u ^ n * (1 - u ^ 2) ^ m
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x * Real.cos x = (Real.cos a ^ 2 - Real.cos b ^ 2) / 2
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x * Real.cos x ^ 2 = (Real.cos a ^ 3 - Real.cos b ^ 3) / 3
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ 3 = Real.cos a - Real.cos b - (Real.cos a ^ 3 - Real.cos b ^ 3) / 3
<VAR>a b : ℝ<VAR>m n : ℕ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ (2 * m) * Real.cos x ^ (2 * n) = ∫ (x : ℝ) in a..b, ((1 - Real.cos (2 * x)) / 2) ^ m * ((1 + Real.cos (2 * x)) / 2) ^ n
<VAR>a b : ℝ<GOAL>∫ (x : ℝ) in a..b, Real.sin x ^ 2 * Real.cos x ^ 2 = (b - a) / 8 - (Real.sin (4 * b) - Real.sin (4 * a)) / 32
<GOAL>∫ (x : ℝ) in -1 ..1, √(1 - x ^ 2) = π / 2
<VAR>E : Type u_1<VAR>SeminormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>p : Subspace ℝ E<VAR>f : ↥p →L[ℝ] ℝ<GOAL>∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>p : Subspace 𝕜 E<VAR>f : ↥p →L[𝕜] 𝕜<GOAL>∃ g, (∀ (x : ↥p), g ↑x = f x) ∧ ‖g‖ = ‖f‖
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>E : Type u_2<VAR>F : Type u_3<VAR>SeminormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : Submodule 𝕜 E<VAR>f : ↥p →L[𝕜] F<VAR>FiniteDimensional 𝕜 ↥(LinearMap.range f)<GOAL>∃ g, f = g.comp p.subtypeL
<VAR>𝕜 : Type u_1<VAR>RCLike 𝕜<VAR>F : Type u_3<VAR>NormedAddCommGroup F<VAR>NormedSpace 𝕜 F<VAR>p : Submodule 𝕜 F<VAR>FiniteDimensional 𝕜 ↥p<GOAL>p.ClosedComplemented
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<GOAL>‖↑‖x‖ • ContinuousLinearEquiv.coord 𝕜 x h‖ = 1
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<VAR>h : x ≠ 0<GOAL>∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>Nontrivial E<VAR>x : E<GOAL>∃ g, ‖g‖ = 1 ∧ g x = ↑‖x‖
<VAR>𝕜 : Type v<VAR>RCLike 𝕜<VAR>E : Type u<VAR>NormedAddCommGroup E<VAR>NormedSpace 𝕜 E<VAR>x : E<GOAL>∃ g, ‖g‖ ≤ 1 ∧ g x = ↑‖x‖
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᴬ[R] Q<GOAL>⇑f.contLinear = ⇑f.linear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᴬ[R] Q<GOAL>↑f.contLinear = f.linear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᵃ[R] Q<VAR>h : Continuous f.toFun<GOAL>⇑{ toAffineMap := f, cont := h }.contLinear = ⇑f.linear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᴬ[R] Q<GOAL>⇑f.linear = ⇑f.contLinear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>W₂ : Type u_5<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>Q₂ : Type u_8<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedAddCommGroup W₂<VAR>MetricSpace Q₂<VAR>NormedAddTorsor W₂ Q₂<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>NormedSpace R W₂<VAR>f : P →ᴬ[R] Q<VAR>g : Q →ᴬ[R] Q₂<GOAL>(g.comp f).contLinear = g.contLinear.comp f.contLinear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᴬ[R] Q<VAR>p : P<VAR>v : V<GOAL>f (v +ᵥ p) = f.contLinear v +ᵥ f p
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᴬ[R] Q<VAR>p₁ p₂ : P<GOAL>f.contLinear (p₁ -ᵥ p₂) = f p₁ -ᵥ f p₂
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>q : Q<GOAL>(ContinuousAffineMap.const R P q).contLinear = 0
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>Q : Type u_7<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>MetricSpace Q<VAR>NormedAddTorsor W Q<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᴬ[R] Q<GOAL>f.contLinear = 0 ↔ ∃ q, f = ContinuousAffineMap.const R P q
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : V →L[R] W<GOAL>f.toContinuousAffineMap.contLinear = f
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<GOAL>ContinuousAffineMap.contLinear 0 = 0
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f g : P →ᴬ[R] W<GOAL>(f + g).contLinear = f.contLinear + g.contLinear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f g : P →ᴬ[R] W<GOAL>(f - g).contLinear = f.contLinear - g.contLinear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : P →ᴬ[R] W<GOAL>(-f).contLinear = -f.contLinear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>P : Type u_6<VAR>NormedAddCommGroup V<VAR>MetricSpace P<VAR>NormedAddTorsor V P<VAR>NormedAddCommGroup W<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>t : R<VAR>f : P →ᴬ[R] W<GOAL>(t • f).contLinear = t • f.contLinear
<VAR>R : Type u_2<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NormedField R<VAR>NormedSpace R V<VAR>NormedSpace R W<VAR>f : V →ᴬ[R] W<GOAL>⇑f = ⇑f.contLinear + Function.const V (f 0)
<VAR>𝕜 : Type u_1<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>f : V →ᴬ[𝕜] W<GOAL>‖f‖ = max ‖f 0‖ ‖f.contLinear‖
<VAR>𝕜 : Type u_1<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>f : V →ᴬ[𝕜] W<GOAL>‖f.contLinear‖ ≤ ‖f‖
<VAR>𝕜 : Type u_1<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>f : V →ᴬ[𝕜] W<GOAL>‖f 0‖ ≤ ‖f‖
<VAR>𝕜 : Type u_1<VAR>V : Type u_3<VAR>W : Type u_4<VAR>NormedAddCommGroup V<VAR>NormedAddCommGroup W<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 V<VAR>NormedSpace 𝕜 W<VAR>f : V →ᴬ[𝕜] W<VAR>h : f 0 = 0<GOAL>‖f‖ = ‖f.contLinear‖