ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<GOAL>∀ x_1 ∈ s ∩ Ico x y, s ∈ 𝓝[>] x_1
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<VAR>z : α<VAR>zs : z ∈ s<VAR>hz : z ∈ Ico x y<GOAL>s ∈ 𝓝[>] z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<VAR>z : α<VAR>zs : z ∈ s<VAR>hz : z ∈ Ico x y<VAR>zt : z ∈ tᶜ<GOAL>s ∈ 𝓝[>] z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<VAR>z : α<VAR>zs : z ∈ s<VAR>hz : z ∈ Ico x y<VAR>zt : z ∈ tᶜ<VAR>this : tᶜ ∩ Ioc z y ∈ 𝓝[>] z<GOAL>s ∈ 𝓝[>] z
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<VAR>z : α<VAR>zs : z ∈ s<VAR>hz : z ∈ Ico x y<VAR>zt : z ∈ tᶜ<VAR>this : tᶜ ∩ Ioc z y ∈ 𝓝[>] z<GOAL>tᶜ ∩ Ioc z y ⊆ s
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>inst✝⁷ : ConditionallyCompleteLinearOrder α<VAR>inst✝⁶ : TopologicalSpace α<VAR>inst✝⁵ : OrderTopology α<VAR>inst✝⁴ : ConditionallyCompleteLinearOrder β<VAR>inst✝³ : TopologicalSpace β<VAR>inst✝² : OrderTopology β<VAR>inst✝¹ : Nonempty γ<VAR>inst✝ : DenselyOrdered α<VAR>a b x y : α<VAR>s t : Set α<VAR>hxy : x ≤ y<VAR>hs : IsClosed s<VAR>ht : IsClosed t<VAR>hab : Icc a b ⊆ s ∪ t<VAR>hx : x ∈ Icc a b ∩ s<VAR>hy : y ∈ Icc a b ∩ t<VAR>xyab : Icc x y ⊆ Icc a b<VAR>hst : ¬(Icc a b ∩ (s ∩ t)).Nonempty<VAR>z : α<VAR>zs : z ∈ s<VAR>hz : z ∈ Ico x y<VAR>zt : z ∈ tᶜ<VAR>this✝ : tᶜ ∩ Ioc z y ∈ 𝓝[>] z<VAR>this : Ioc z y ⊆ s ∪ t<GOAL>tᶜ ∩ Ioc z y ⊆ s
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : PredOrder α<VAR>h : IsPredLimit (pred a)<GOAL>IsMin a
<VAR>α : Type u_1<VAR>inst✝¹ : Preorder α<VAR>a : α<VAR>inst✝ : PredOrder α<VAR>h : IsPredLimit (pred a)<VAR>H : ¬IsMin a<GOAL>False
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>μ : K<VAR>hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ<GOAL>∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>μ : K<VAR>hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ<VAR>h✝ : IsEmpty n<GOAL>∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
<VAR>K : Type u_1<VAR>n : Type u_2<VAR>inst✝² : NormedField K<VAR>inst✝¹ : Fintype n<VAR>inst✝ : DecidableEq n<VAR>A : Matrix n n K<VAR>μ : K<VAR>hμ : Module.End.HasEigenvalue (Matrix.toLin' A) μ<VAR>h✝ : Nonempty n<GOAL>∃ k, μ ∈ Metric.closedBall (A k k) (∑ j ∈ Finset.univ.erase k, ‖A k j‖)
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>ts' : ι → TopologicalSpace E<VAR>h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E<GOAL>LocallyConvexSpace 𝕜 E
<VAR>ι : Sort u_1<VAR>𝕜 : Type u_2<VAR>E : Type u_3<VAR>F : Type u_4<VAR>inst✝⁴ : OrderedSemiring 𝕜<VAR>inst✝³ : AddCommMonoid E<VAR>inst✝² : Module 𝕜 E<VAR>inst✝¹ : AddCommMonoid F<VAR>inst✝ : Module 𝕜 F<VAR>ts' : ι → TopologicalSpace E<VAR>h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E<GOAL>∀ t ∈ range fun i => ts' i, LocallyConvexSpace 𝕜 E
<VAR>𝕜 : Type u<VAR>inst✝⁴ : NontriviallyNormedField 𝕜<VAR>F : Type v<VAR>inst✝³ : NormedAddCommGroup F<VAR>inst✝² : NormedSpace 𝕜 F<VAR>E : Type w<VAR>inst✝¹ : NormedAddCommGroup E<VAR>inst✝ : NormedSpace 𝕜 E<VAR>f f₀ f₁ g : 𝕜 → F<VAR>f' f₀' f₁' g' : F<VAR>x : 𝕜<VAR>s t✝ : Set 𝕜<VAR>L L₁ L₂ : Filter 𝕜<VAR>l : F → E<VAR>l' : F →L[𝕜] E<VAR>y : F<VAR>t : Set F<VAR>hl : HasFDerivWithinAt l l' t (f x)<VAR>hf : HasDerivWithinAt f f' s x<VAR>hst : MapsTo f s t<VAR>hy : y = f x<GOAL>HasDerivWithinAt (l ∘ f) (l' f') s x
<VAR>R : Type u<VAR>S✝ : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<VAR>x✝ : A<GOAL>x✝ ∈ LinearMap.range (toAlgHom R (↥S) A) ↔ x✝ ∈ toSubmodule S
<VAR>R : Type u<VAR>S✝ : Type v<VAR>A : Type w<VAR>B : Type u₁<VAR>M : Type v₁<VAR>inst✝² : CommSemiring R<VAR>inst✝¹ : CommSemiring A<VAR>inst✝ : Algebra R A<VAR>S : Subalgebra R A<VAR>x✝ : A<GOAL>(∃ y, (algebraMap (↥S) A) y = x✝) ↔ ∃ y, (toSubmodule S).subtype y = x✝
<VAR>X : Type u_1<VAR>Y : Type u_2<VAR>inst✝² : TopologicalSpace X<VAR>inst✝¹ : FirstCountableTopology X<VAR>inst✝ : R1Space X<VAR>x y : X<GOAL>IsClosed {p | Inseparable p.1 p.2}
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>h1 : c ≤ a<VAR>h2 : c ≤ b<GOAL>a - c = b - c ↔ a = b
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>IsPurelyInseparable F E ↔ perfectClosure F E = ⊤
<VAR>F : Type u<VAR>E : Type v<VAR>inst✝⁴ : Field F<VAR>inst✝³ : Field E<VAR>inst✝² : Algebra F E<VAR>K : Type w<VAR>inst✝¹ : Field K<VAR>inst✝ : Algebra F K<GOAL>(∀ (x : E), ∃ n, x ^ ringExpChar F ^ n ∈ (algebraMap F E).range) ↔ perfectClosure F E = ⊤
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>l : List α<VAR>n : ℕ<GOAL>l.enum[n]? = Option.map (fun a => (n, a)) l[n]?
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ol : l.Bounded o₁ ↑x<VAR>Or : r.Bounded (↑x) o₂<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>b : BalancedSz l.size r.size<VAR>bl : l.Balanced<VAR>br : r.Balanced<VAR>ol' : l.dual.Bounded (↑x) o₁<VAR>sl' : l.dual.Sized<VAR>bl' : l.dual.Balanced<VAR>or' : r.dual.Bounded o₂ ↑x<VAR>sr' : r.dual.Sized<VAR>br' : r.dual.Balanced<GOAL>l.size + r.size + 1 = r.dual.size + l.dual.size + 1
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ol : l.Bounded o₁ ↑x<VAR>Or : r.Bounded (↑x) o₂<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>b : BalancedSz l.size r.size<VAR>bl : l.Balanced<VAR>br : r.Balanced<VAR>ol' : l.dual.Bounded (↑x) o₁<VAR>sl' : l.dual.Sized<VAR>bl' : l.dual.Balanced<VAR>or' : r.dual.Bounded o₂ ↑x<VAR>sr' : r.dual.Sized<VAR>br' : r.dual.Balanced<GOAL>BalancedSz r.dual.size l.dual.size
<VAR>α : Type u_1<VAR>inst✝ : Preorder α<VAR>l : Ordnode α<VAR>x : α<VAR>r : Ordnode α<VAR>o₁ : WithBot α<VAR>o₂ : WithTop α<VAR>ol : l.Bounded o₁ ↑x<VAR>Or : r.Bounded (↑x) o₂<VAR>sl : l.Sized<VAR>sr : r.Sized<VAR>b : BalancedSz l.size r.size<VAR>bl : l.Balanced<VAR>br : r.Balanced<VAR>ol' : l.dual.Bounded (↑x) o₁<VAR>sl' : l.dual.Sized<VAR>bl' : l.dual.Balanced<VAR>or' : r.dual.Bounded o₂ ↑x<VAR>sr' : r.dual.Sized<VAR>br' : r.dual.Balanced<GOAL>BalancedSz r.size l.size
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : List α<GOAL>toList xs = xs
<VAR>α β γ : Type u<VAR>t : Type u → Type u<VAR>inst✝¹ : Traversable t<VAR>inst✝ : LawfulTraversable t<VAR>xs : List α<GOAL>FreeMonoid.toList (List.traverse (Const.mk' ∘ FreeMonoid.of) xs) = xs
<VAR>α : Type u_1<VAR>inst✝⁵ : AddCommSemigroup α<VAR>inst✝⁴ : PartialOrder α<VAR>inst✝³ : ExistsAddOfLE α<VAR>inst✝² : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1<VAR>inst✝¹ : Sub α<VAR>inst✝ : OrderedSub α<VAR>a b c d : α<VAR>hc : AddLECancellable c<VAR>h : c ≤ b<GOAL>a < b - c ↔ c + a < b
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<GOAL>Continuous fun f => ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<GOAL>∀ (x : ↥(Lp E 1 (μ.prod ν))), ContinuousAt (fun f => ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ) x
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<GOAL>ContinuousAt (fun f => ∫ (x : α), ∫ (y : β), ↑↑f (x, y) ∂ν ∂μ) g
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<GOAL>Tendsto (fun i => ∫⁻ (x : α), ↑‖∫ (y : β), ↑↑i (x, y) ∂ν - ∫ (y : β), ↑↑g (x, y) ∂ν‖₊ ∂μ) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<GOAL>Tendsto (fun i => ∫⁻ (x : α), ↑‖∫ (y : β), ↑↑i (x, y) - ↑↑g (x, y) ∂ν‖₊ ∂μ) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<GOAL>↥(Lp E 1 (μ.prod ν)) → ℝ≥0∞
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<GOAL>Tendsto ?m.114467 (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<GOAL>(fun i => ∫⁻ (x : α), ↑‖∫ (y : β), ↑↑i (x, y) - ↑↑g (x, y) ∂ν‖₊ ∂μ) ≤ ?m.114467
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<GOAL>Tendsto (fun i => ∫⁻ (x : α), ∫⁻ (y : β), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂ν ∂μ) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<VAR>this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun i => ∫⁻ (x : α), ∫⁻ (y : β), ↑‖↑↑i (x, y) - ↑↑g (x, y)‖₊ ∂ν ∂μ) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<VAR>this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun x => ENNReal.ofReal ‖x - g‖) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<VAR>this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun x => ENNReal.ofReal ‖x - g‖) (𝓝 g) (𝓝 (ENNReal.ofReal 0))
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<VAR>this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun x => ‖x - g‖) (𝓝 g) (𝓝 0)
<VAR>α : Type u_1<VAR>α' : Type u_2<VAR>β : Type u_3<VAR>β' : Type u_4<VAR>γ : Type u_5<VAR>E : Type u_6<VAR>inst✝¹⁰ : MeasurableSpace α<VAR>inst✝⁹ : MeasurableSpace α'<VAR>inst✝⁸ : MeasurableSpace β<VAR>inst✝⁷ : MeasurableSpace β'<VAR>inst✝⁶ : MeasurableSpace γ<VAR>μ μ' : Measure α<VAR>ν ν' : Measure β<VAR>τ : Measure γ<VAR>inst✝⁵ : NormedAddCommGroup E<VAR>inst✝⁴ : SFinite ν<VAR>inst✝³ : NormedSpace ℝ E<VAR>inst✝² : SFinite μ<VAR>E' : Type u_7<VAR>inst✝¹ : NormedAddCommGroup E'<VAR>inst✝ : NormedSpace ℝ E'<VAR>g : ↥(Lp E 1 (μ.prod ν))<VAR>this : ∀ (i : ↥(Lp E 1 (μ.prod ν))), Measurable fun z => ↑‖↑↑i z - ↑↑g z‖₊<GOAL>Tendsto (fun x => x) (𝓝 g) (𝓝 g)
<VAR>α : Type u_1<VAR>β : Type u_2<VAR>δ : Type u_3<VAR>inst✝³ : MeasurableSpace α<VAR>inst✝² : MeasurableSpace β<VAR>s : Set α<VAR>a : α<VAR>inst✝¹ : Countable α<VAR>inst✝ : MeasurableSingletonClass α<VAR>μ : Measure α<GOAL>(sum fun a => μ {a} • dirac a) = μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<GOAL>μ ≪ map (fun x => x * g) μ
<VAR>G : Type u_1<VAR>inst✝⁶ : MeasurableSpace G<VAR>inst✝⁵ : Group G<VAR>inst✝⁴ : MeasurableMul₂ G<VAR>μ ν : Measure G<VAR>inst✝³ : SFinite ν<VAR>inst✝² : SFinite μ<VAR>s✝ : Set G<VAR>inst✝¹ : MeasurableInv G<VAR>inst✝ : μ.IsMulLeftInvariant<VAR>g : G<VAR>s : Set G<VAR>hs : MeasurableSet s<GOAL>(map (fun x => x * g) μ) s = 0 → μ s = 0
<VAR>T : Type uT<VAR>g : ContextFreeGrammar T<VAR>v w : List (Symbol T g.NT)<VAR>hvw : g.Derives v w<VAR>p : List (Symbol T g.NT)<GOAL>g.Derives (p ++ v) (p ++ w)
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<GOAL>Memℓp (-f) p
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f 0<GOAL>Memℓp (-f) 0
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f ⊤<GOAL>Memℓp (-f) ⊤
<VAR>α : Type u_1<VAR>E : α → Type u_2<VAR>p q : ℝ≥0∞<VAR>inst✝ : (i : α) → NormedAddCommGroup (E i)<VAR>f : (i : α) → E i<VAR>hf : Memℓp f p<VAR>hp : 0 < p.toReal<GOAL>Memℓp (-f) p
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy : y = 0 → x = 0 ∨ z = 0<GOAL>SameRay R x z
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>y z : M<VAR>hyz : SameRay R y z<VAR>hxy : SameRay R 0 y<VAR>hy : y = 0 → 0 = 0 ∨ z = 0<GOAL>SameRay R 0 z
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy : y = 0 → x = 0 ∨ z = 0<VAR>hx : x ≠ 0<GOAL>SameRay R x z
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y : M<VAR>hxy : SameRay R x y<VAR>hx : x ≠ 0<VAR>hyz : SameRay R y 0<VAR>hy : y = 0 → x = 0 ∨ 0 = 0<GOAL>SameRay R x 0
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy : y = 0 → x = 0 ∨ z = 0<VAR>hx : x ≠ 0<VAR>hz : z ≠ 0<GOAL>SameRay R x z
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x z : M<VAR>hx : x ≠ 0<VAR>hz : z ≠ 0<VAR>hxy : SameRay R x 0<VAR>hyz : SameRay R 0 z<VAR>hy : 0 = 0 → x = 0 ∨ z = 0<GOAL>SameRay R x z
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy✝ : y = 0 → x = 0 ∨ z = 0<VAR>hx : x ≠ 0<VAR>hz : z ≠ 0<VAR>hy : y ≠ 0<GOAL>SameRay R x z
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy✝ : y = 0 → x = 0 ∨ z = 0<VAR>hx : x ≠ 0<VAR>hz : z ≠ 0<VAR>hy : y ≠ 0<VAR>r₁ r₂ : R<VAR>hr₁ : 0 < r₁<VAR>hr₂ : 0 < r₂<VAR>h₁ : r₁ • x = r₂ • y<GOAL>SameRay R x z
<VAR>R : Type u_1<VAR>inst✝⁵ : StrictOrderedCommSemiring R<VAR>M : Type u_2<VAR>inst✝⁴ : AddCommMonoid M<VAR>inst✝³ : Module R M<VAR>N : Type u_3<VAR>inst✝² : AddCommMonoid N<VAR>inst✝¹ : Module R N<VAR>ι : Type u_4<VAR>inst✝ : DecidableEq ι<VAR>x y z : M<VAR>hxy : SameRay R x y<VAR>hyz : SameRay R y z<VAR>hy✝ : y = 0 → x = 0 ∨ z = 0<VAR>hx : x ≠ 0<VAR>hz : z ≠ 0<VAR>hy : y ≠ 0<VAR>r₁ r₂ : R<VAR>hr₁ : 0 < r₁<VAR>hr₂ : 0 < r₂<VAR>h₁ : r₁ • x = r₂ • y<VAR>r₃ r₄ : R<VAR>hr₃ : 0 < r₃<VAR>hr₄ : 0 < r₄<VAR>h₂ : r₃ • y = r₄ • z<GOAL>SameRay R x z