ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ioo (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Icc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ico (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ioc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Icc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Ico (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Ioc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ioc A B)) l fun i => Set.Ioo (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Icc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Ico (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Ioc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Ico A B)) l fun i => Set.Ioo (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Icc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Ico (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Ioc (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>LinearOrder α<VAR>TopologicalSpace α<VAR>OrderClosedTopology α<VAR>OpensMeasurableSpace α<VAR>a b : ι → α<VAR>A B : α<VAR>MeasureTheory.NoAtoms μ<VAR>ha : Filter.Tendsto a l (𝓝 A)<VAR>hb : Filter.Tendsto b l (𝓝 B)<GOAL>MeasureTheory.AECover (μ.restrict (Set.Icc A B)) l fun i => Set.Ioo (a i) (b i)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>s : Set α<GOAL>MeasureTheory.AECover (μ.restrict s) l φ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>s : Set α<VAR>φ : ι → Set α<VAR>hs : MeasurableSet s<VAR>ae_eventually_mem : ∀ᵐ (x : α) ∂μ, x ∈ s → ∀ᶠ (n : ι) in l, x ∈ φ n<VAR>measurable : ∀ (n : ι), MeasurableSet (φ n)<GOAL>MeasureTheory.AECover (μ.restrict s) l φ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>s : Set α<VAR>hs : MeasurableSet s<GOAL>MeasureTheory.AECover (μ.restrict s) l fun i => φ i ∩ s
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>Zero β<VAR>TopologicalSpace β<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<GOAL>∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun i => (φ i).indicator f x) l (𝓝 (f x))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>MeasurableSpace β<VAR>l.IsCountablyGenerated<VAR>l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>hfm : ∀ (i : ι), AEMeasurable f (μ.restrict (φ i))<GOAL>AEMeasurable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>β : Type u_3<VAR>TopologicalSpace β<VAR>TopologicalSpace.PseudoMetrizableSpace β<VAR>l.IsCountablyGenerated<VAR>l.NeBot<VAR>f : α → β<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>hfm : ∀ (i : ι), MeasureTheory.AEStronglyMeasurable f (μ.restrict (φ i))<GOAL>MeasureTheory.AEStronglyMeasurable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>ι' : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>l' : Filter ι'<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>u : ι' → ι<VAR>hu : Filter.Tendsto u l' l<GOAL>MeasureTheory.AECover μ l' (φ ∘ u)
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>Countable ι<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Preorder ι<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ Filter.atTop φ<GOAL>MeasureTheory.AECover μ Filter.atTop fun n => ⋃ k ∈ Set.Iic n, φ k
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>Countable ι<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>Preorder ι<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ Filter.atTop φ<GOAL>MeasureTheory.AECover μ Filter.atTop fun n => ⋂ k ∈ Set.Ici n, φ k
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>φ : ℕ → Set α<VAR>hφ : MeasureTheory.AECover μ Filter.atTop φ<VAR>hmono : Monotone φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<GOAL>Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) Filter.atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>φ : ℕ → Set α<VAR>hφ : MeasureTheory.AECover μ Filter.atTop φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<GOAL>Filter.Tendsto (fun x => ∫⁻ (x : α) in φ x, f x ∂μ) Filter.atTop (𝓝 (∫⁻ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<GOAL>Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 (∫⁻ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>I : ℝ≥0∞<VAR>hfm : AEMeasurable f μ<VAR>htendsto : Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (𝓝 I)<GOAL>∫⁻ (x : α), f x ∂μ = I
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>Nonempty ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → ℝ≥0∞<VAR>hfm : AEMeasurable f μ<GOAL>⨆ i, ∫⁻ (x : α) in φ i, f x ∂μ = ∫⁻ (x : α), f x ∂μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<VAR>htendsto : Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 (ENNReal.ofReal I))<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>I : ℝ≥0<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ↑I<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>I : ℝ≥0<VAR>hfm : MeasureTheory.AEStronglyMeasurable f μ<VAR>htendsto : Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ) l (𝓝 ↑I)<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ<VAR>htendsto : Filter.Tendsto (fun i => ∫ (x : α) in φ i, ‖f x‖ ∂μ) l (𝓝 I)<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → ℝ<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ<VAR>hnng : ∀ᵐ (x : α) ∂μ, 0 ≤ f x<VAR>hbounded : ∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, f x ∂μ ≤ I<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → ℝ<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ<VAR>hnng : ∀ᵐ (x : α) ∂μ, 0 ≤ f x<VAR>htendsto : Filter.Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (𝓝 I)<GOAL>MeasureTheory.Integrable f μ
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>hfi : MeasureTheory.Integrable f μ<GOAL>Filter.Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (𝓝 (∫ (x : α), f x ∂μ))
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>E : Type u_3<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → E<VAR>I : E<VAR>hfi : MeasureTheory.Integrable f μ<VAR>h : Filter.Tendsto (fun n => ∫ (x : α) in φ n, f x ∂μ) l (𝓝 I)<GOAL>∫ (x : α), f x ∂μ = I
<VAR>α : Type u_1<VAR>ι : Type u_2<VAR>MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>φ : ι → Set α<VAR>hφ : MeasureTheory.AECover μ l φ<VAR>f : α → ℝ<VAR>I : ℝ<VAR>hnng : 0 ≤ᵐ[μ] f<VAR>hfi : ∀ (n : ι), MeasureTheory.IntegrableOn f (φ n) μ<VAR>htendsto : Filter.Tendsto (fun n => ∫ (x : α) in φ n, f x ∂μ) l (𝓝 I)<GOAL>∫ (x : α), f x ∂μ = I
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ ≤ I<GOAL>MeasureTheory.Integrable f μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>h : Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) l (𝓝 I)<GOAL>MeasureTheory.Integrable f μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>a : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ ≤ I<GOAL>MeasureTheory.IntegrableOn f (Set.Iic b) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>a : ι → ℝ<VAR>f : ℝ → E<VAR>I b : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>h : Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ) l (𝓝 I)<GOAL>MeasureTheory.IntegrableOn f (Set.Iic b) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ ≤ I<GOAL>MeasureTheory.IntegrableOn f (Set.Ioi a) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>b : ι → ℝ<VAR>f : ℝ → E<VAR>I a : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ<VAR>hb : Filter.Tendsto b l Filter.atTop<VAR>h : Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) l (𝓝 I)<GOAL>MeasureTheory.IntegrableOn f (Set.Ioi a) μ
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>I a₀ b₀ : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) MeasureTheory.volume<VAR>ha : Filter.Tendsto a l (𝓝 a₀)<VAR>hb : Filter.Tendsto b l (𝓝 b₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Set.Ioc (a i) (b i), ‖f x‖ ≤ I<GOAL>MeasureTheory.IntegrableOn f (Set.Ioc a₀ b₀) MeasureTheory.volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>a : ι → ℝ<VAR>f : ℝ → E<VAR>I a₀ b : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) MeasureTheory.volume<VAR>ha : Filter.Tendsto a l (𝓝 a₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Set.Ioc (a i) b, ‖f x‖ ≤ I<GOAL>MeasureTheory.IntegrableOn f (Set.Ioc a₀ b) MeasureTheory.volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>l : Filter ι<VAR>l.NeBot<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>b : ι → ℝ<VAR>f : ℝ → E<VAR>I a b₀ : ℝ<VAR>hfi : ∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) MeasureTheory.volume<VAR>hb : Filter.Tendsto b l (𝓝 b₀)<VAR>h : ∀ᶠ (i : ι) in l, ∫ (x : ℝ) in Set.Ioc a (b i), ‖f x‖ ≤ I<GOAL>MeasureTheory.IntegrableOn f (Set.Ioc a b₀) MeasureTheory.volume
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a b : ι → ℝ<VAR>f : ℝ → E<VAR>hfi : MeasureTheory.Integrable f μ<VAR>ha : Filter.Tendsto a l Filter.atBot<VAR>hb : Filter.Tendsto b l Filter.atTop<GOAL>Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ), f x ∂μ))
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>a : ι → ℝ<VAR>f : ℝ → E<VAR>b : ℝ<VAR>hfi : MeasureTheory.IntegrableOn f (Set.Iic b) μ<VAR>ha : Filter.Tendsto a l Filter.atBot<GOAL>Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Set.Iic b, f x ∂μ))
<VAR>ι : Type u_1<VAR>E : Type u_2<VAR>μ : MeasureTheory.Measure ℝ<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>b : ι → ℝ<VAR>f : ℝ → E<VAR>a : ℝ<VAR>hfi : MeasureTheory.IntegrableOn f (Set.Ioi a) μ<VAR>hb : Filter.Tendsto b l Filter.atTop<GOAL>Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (𝓝 (∫ (x : ℝ) in Set.Ioi a, f x ∂μ))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume<GOAL>Filter.Tendsto f Filter.atTop (𝓝 (limUnder Filter.atTop f))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume<VAR>fint : MeasureTheory.IntegrableOn f (Set.Ioi a) MeasureTheory.volume<GOAL>Filter.Tendsto f Filter.atTop (𝓝 0)
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>m : E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hcont : ContinuousWithinAt f (Set.Ici a) a<VAR>hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 m)<GOAL>∫ (x : ℝ) in Set.Ioi a, f' x = m - f a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>m : E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hderiv : ∀ x ∈ Set.Ici a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume<VAR>hf : Filter.Tendsto f Filter.atTop (𝓝 m)<GOAL>∫ (x : ℝ) in Set.Ioi a, f' x = m - f a
<VAR>E : Type u_1<VAR>f : ℝ → E<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hf : ContDiff ℝ 1 f<VAR>h2f : HasCompactSupport f<VAR>b : ℝ<GOAL>∫ (x : ℝ) in Set.Ioi b, deriv f x = -f b
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hcont : ContinuousWithinAt g (Set.Ici a) a<VAR>hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hderiv : ∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hcont : ContinuousWithinAt g (Set.Ici a) a<VAR>hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hderiv : ∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x<VAR>g'pos : ∀ x ∈ Set.Ioi a, 0 ≤ g' x<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hcont : ContinuousWithinAt g (Set.Ici a) a<VAR>hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hderiv : ∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hcont : ContinuousWithinAt g (Set.Ici a) a<VAR>hderiv : ∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
<VAR>g g' : ℝ → ℝ<VAR>a l : ℝ<VAR>hderiv : ∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x<VAR>g'neg : ∀ x ∈ Set.Ioi a, g' x ≤ 0<VAR>hg : Filter.Tendsto g Filter.atTop (𝓝 l)<GOAL>∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>CompleteSpace E<VAR>hderiv : ∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume<GOAL>Filter.Tendsto f Filter.atBot (𝓝 (limUnder Filter.atBot f))
<VAR>E : Type u_1<VAR>f f' : ℝ → E<VAR>a : ℝ<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>hderiv : ∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x<VAR>f'int : MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume<VAR>fint : MeasureTheory.IntegrableOn f (Set.Iic a) MeasureTheory.volume<GOAL>Filter.Tendsto f Filter.atBot (𝓝 0)