ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f g : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<GOAL>MeasureTheory.setToFun μ T hT (f - g) = MeasureTheory.setToFun μ T hT f - MeasureTheory.setToFun μ T hT g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>𝕜 : Type u_6<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>NontriviallyNormedField 𝕜<VAR>NormedSpace 𝕜 E<VAR>NormedSpace 𝕜 F<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h_smul : ∀ (c : 𝕜) (s : Set α) (x : E), (T s) (c • x) = c • (T s) x<VAR>c : 𝕜<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T hT (c • f) = c • MeasureTheory.setToFun μ T hT f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f g : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h : f =ᵐ[μ] g<GOAL>MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ T hT g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h : μ = 0<GOAL>MeasureTheory.setToFun μ T hT f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → μ s = 0<GOAL>MeasureTheory.setToFun μ T hT f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.setToFun μ T hT ↑↑(MeasureTheory.Integrable.toL1 f hf) = MeasureTheory.setToFun μ T hT f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>hμs : μ s ≠ ⊤<VAR>x : E<GOAL>MeasureTheory.setToFun μ T hT (s.indicator fun x_1 => x) = (T s) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>MeasureTheory.IsFiniteMeasure μ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>x : E<GOAL>(MeasureTheory.setToFun μ T hT fun x_1 => x) = (T Set.univ) x
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>T T' : Set α → E →L[ℝ] G''<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hTT' : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : E), (T s) x ≤ (T' s) x<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T hT f ≤ MeasureTheory.setToFun μ T' hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>T T' : Set α → E →L[ℝ] G''<VAR>C C' : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C'<VAR>hTT' : ∀ (s : Set α) (x : E), (T s) x ≤ (T' s) x<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>MeasureTheory.setToFun μ T hT ↑↑f ≤ MeasureTheory.setToFun μ T' hT' ↑↑f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>NormedLatticeAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f : α → G'<VAR>hf : 0 ≤ᵐ[μ] f<GOAL>0 ≤ MeasureTheory.setToFun μ T hT f
<VAR>α : Type u_1<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>G' : Type u_7<VAR>G'' : Type u_8<VAR>NormedLatticeAddCommGroup G''<VAR>NormedSpace ℝ G''<VAR>CompleteSpace G''<VAR>NormedLatticeAddCommGroup G'<VAR>NormedSpace ℝ G'<VAR>T : Set α → G' →L[ℝ] G''<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT_nonneg : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∀ (x : G'), 0 ≤ x → 0 ≤ (T s) x<VAR>f g : α → G'<VAR>hf : MeasureTheory.Integrable f μ<VAR>hg : MeasureTheory.Integrable g μ<VAR>hfg : f ≤ᵐ[μ] g<GOAL>MeasureTheory.setToFun μ T hT f ≤ MeasureTheory.setToFun μ T hT g
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<GOAL>Continuous fun f => MeasureTheory.setToFun μ T hT ↑↑f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>f : α → E<VAR>hfi : MeasureTheory.Integrable f μ<VAR>fs : ι → α → E<VAR>l : Filter ι<VAR>hfsi : ∀ᶠ (i : ι) in l, MeasureTheory.Integrable (fs i) μ<VAR>hfs : Filter.Tendsto (fun i => ∫⁻ (x : α), ↑‖fs i x - f x‖₊ ∂μ) l (𝓝 0)<GOAL>Filter.Tendsto (fun i => MeasureTheory.setToFun μ T hT (fs i)) l (𝓝 (MeasureTheory.setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → E<VAR>s : Set E<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hfi : MeasureTheory.Integrable f μ<VAR>hfm : Measurable f<VAR>hs : ∀ᵐ (x : α) ∂μ, f x ∈ closure s<VAR>y₀ : E<VAR>h₀ : y₀ ∈ s<VAR>h₀i : MeasureTheory.Integrable (fun x => y₀) μ<GOAL>Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT ↑(MeasureTheory.SimpleFunc.approxOn f hfm s y₀ h₀ n)) Filter.atTop (𝓝 (MeasureTheory.setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>MeasurableSpace E<VAR>BorelSpace E<VAR>f : α → E<VAR>fmeas : Measurable f<VAR>hf : MeasureTheory.Integrable f μ<VAR>s : Set E<VAR>TopologicalSpace.SeparableSpace ↑s<VAR>hs : Set.range f ∪ {0} ⊆ s<GOAL>Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT ↑(MeasureTheory.SimpleFunc.approxOn f fmeas s 0 ⋯ n)) Filter.atTop (𝓝 (MeasureTheory.setToFun μ T hT f))
<VAR>α : Type u_1<VAR>G : Type u_5<VAR>NormedAddCommGroup G<VAR>m : MeasurableSpace α<VAR>μ μ' : MeasureTheory.Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<GOAL>Continuous fun f => MeasureTheory.Integrable.toL1 ↑↑f ⋯
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>μ' : MeasureTheory.Measure α<VAR>c' : ℝ≥0∞<VAR>hc' : c' ≠ ⊤<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<VAR>hfμ : MeasureTheory.Integrable f μ<GOAL>MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ' T hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>μ' : MeasureTheory.Measure α<VAR>c c' : ℝ≥0∞<VAR>hc : c ≠ ⊤<VAR>hc' : c' ≠ ⊤<VAR>hμ_le : μ ≤ c • μ'<VAR>hμ'_le : μ' ≤ c' • μ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT' : MeasureTheory.DominatedFinMeasAdditive μ' T C'<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun μ' T hT' f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>μ' : MeasureTheory.Measure α<VAR>hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f (μ + μ')<GOAL>MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ T hT f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>μ' : MeasureTheory.Measure α<VAR>hT_add : MeasureTheory.DominatedFinMeasAdditive (μ + μ') T C'<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ' T C<VAR>f : α → E<VAR>hf : MeasureTheory.Integrable f (μ + μ')<GOAL>MeasureTheory.setToFun (μ + μ') T hT_add f = MeasureTheory.setToFun μ' T hT f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive (⊤ • μ) T C<VAR>f : α → E<GOAL>MeasureTheory.setToFun (⊤ • μ) T hT f = 0
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C C' : ℝ<VAR>c : ℝ≥0∞<VAR>hc_ne_top : c ≠ ⊤<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hT_smul : MeasureTheory.DominatedFinMeasAdditive (c • μ) T C'<VAR>f : α → E<GOAL>MeasureTheory.setToFun μ T hT f = MeasureTheory.setToFun (c • μ) T hT_smul f
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<VAR>hC : 0 ≤ C<GOAL>‖MeasureTheory.setToFun μ T hT ↑↑f‖ ≤ C * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>f : ↥(MeasureTheory.Lp E 1 μ)<GOAL>‖MeasureTheory.setToFun μ T hT ↑↑f‖ ≤ max C 0 * ‖f‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : MeasureTheory.Integrable f μ<VAR>hC : 0 ≤ C<GOAL>‖MeasureTheory.setToFun μ T hT f‖ ≤ C * ‖MeasureTheory.Integrable.toL1 f hf‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>f : α → E<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>hf : MeasureTheory.Integrable f μ<GOAL>‖MeasureTheory.setToFun μ T hT f‖ ≤ max C 0 * ‖MeasureTheory.Integrable.toL1 f hf‖
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>fs : ℕ → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>fs_measurable : ∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (fs n) μ<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_bound : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => fs n a) Filter.atTop (𝓝 (f a))<GOAL>Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT (fs n)) Filter.atTop (𝓝 (MeasureTheory.setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>ι : Type u_7<VAR>l : Filter ι<VAR>l.IsCountablyGenerated<VAR>fs : ι → α → E<VAR>f : α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (fs n) μ<VAR>h_bound : ∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖fs n a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_lim : ∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => fs n a) l (𝓝 (f a))<GOAL>Filter.Tendsto (fun n => MeasureTheory.setToFun μ T hT (fs n)) l (𝓝 (MeasureTheory.setToFun μ T hT f))
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>X : Type u_7<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>fs : X → α → E<VAR>x₀ : X<VAR>bound : α → ℝ<VAR>s : Set X<VAR>hfs_meas : ∀ᶠ (x : X) in 𝓝[s] x₀, MeasureTheory.AEStronglyMeasurable (fs x) μ<VAR>h_bound : ∀ᶠ (x : X) in 𝓝[s] x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, ContinuousWithinAt (fun x => fs x a) s x₀<GOAL>ContinuousWithinAt (fun x => MeasureTheory.setToFun μ T hT (fs x)) s x₀
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>X : Type u_7<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>fs : X → α → E<VAR>x₀ : X<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ᶠ (x : X) in 𝓝 x₀, MeasureTheory.AEStronglyMeasurable (fs x) μ<VAR>h_bound : ∀ᶠ (x : X) in 𝓝 x₀, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, ContinuousAt (fun x => fs x a) x₀<GOAL>ContinuousAt (fun x => MeasureTheory.setToFun μ T hT (fs x)) x₀
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>X : Type u_7<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>fs : X → α → E<VAR>bound : α → ℝ<VAR>s : Set X<VAR>hfs_meas : ∀ x ∈ s, MeasureTheory.AEStronglyMeasurable (fs x) μ<VAR>h_bound : ∀ x ∈ s, ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, ContinuousOn (fun x => fs x a) s<GOAL>ContinuousOn (fun x => MeasureTheory.setToFun μ T hT (fs x)) s
<VAR>α : Type u_1<VAR>E : Type u_2<VAR>F : Type u_3<VAR>NormedAddCommGroup E<VAR>NormedSpace ℝ E<VAR>NormedAddCommGroup F<VAR>NormedSpace ℝ F<VAR>m : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>CompleteSpace F<VAR>T : Set α → E →L[ℝ] F<VAR>C : ℝ<VAR>X : Type u_7<VAR>TopologicalSpace X<VAR>FirstCountableTopology X<VAR>hT : MeasureTheory.DominatedFinMeasAdditive μ T C<VAR>fs : X → α → E<VAR>bound : α → ℝ<VAR>hfs_meas : ∀ (x : X), MeasureTheory.AEStronglyMeasurable (fs x) μ<VAR>h_bound : ∀ (x : X), ∀ᵐ (a : α) ∂μ, ‖fs x a‖ ≤ bound a<VAR>bound_integrable : MeasureTheory.Integrable bound μ<VAR>h_cont : ∀ᵐ (a : α) ∂μ, Continuous fun x => fs x a<GOAL>Continuous fun x => MeasureTheory.setToFun μ T hT (fs x)
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>s : Set α<VAR>μ : MeasureTheory.Measure α<GOAL>(MeasureTheory.Measure.restrictₗ s) μ = μ.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : MeasurableSet s<GOAL>(μ.restrict s).toOuterMeasure = (MeasureTheory.OuterMeasure.restrict s) μ.toOuterMeasure
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : MeasureTheory.NullMeasurableSet t (μ.restrict s)<GOAL>(μ.restrict s) t = μ (t ∩ s)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict s) t = μ (t ∩ s)
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>s s' : Set α<VAR>μ ν : MeasureTheory.Measure α<VAR>hs : s ≤ᵐ[μ] s'<VAR>hμν : μ ≤ ν<GOAL>μ.restrict s ≤ ν.restrict s'
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>s s' : Set α<VAR>hs : s ⊆ s'<VAR>μ ν : MeasureTheory.Measure α<VAR>hμν : μ ≤ ν<GOAL>μ.restrict s ≤ ν.restrict s'
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : s ≤ᵐ[μ] t<GOAL>μ.restrict s ≤ μ.restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : s =ᵐ[μ] t<GOAL>μ.restrict s = μ.restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict s) t = μ (t ∩ s)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s μ<GOAL>(μ.restrict s) t = μ (t ∩ s)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ.restrict s ≤ μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>(μ.restrict t) s = μ s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(μ.restrict s) s = μ s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(μ.restrict s) Set.univ = μ s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>μ (t ∩ s) ≤ (μ.restrict s) t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<GOAL>(μ.restrict s) t ≤ μ t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>(μ.restrict s) t = μ s
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>μ ν : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(μ + ν).restrict s = μ.restrict s + ν.restrict s
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>s : Set α<GOAL>MeasureTheory.Measure.restrict 0 s = 0
<VAR>α : Type u_2<VAR>_m0 : MeasurableSpace α<VAR>c : ℝ≥0∞<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>(c • μ).restrict s = c • μ.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasureTheory.NullMeasurableSet s (μ.restrict t)<GOAL>(μ.restrict t).restrict s = μ.restrict (s ∩ t)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict t).restrict s = μ.restrict (s ∩ t)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : s ⊆ t<GOAL>(μ.restrict t).restrict s = μ.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>(μ.restrict t).restrict s = μ.restrict (s ∩ t)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict t).restrict s = μ.restrict (s ∩ t)
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict t).restrict s = (μ.restrict s).restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>ht : MeasurableSet t<GOAL>(μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : (μ.restrict s) t = 0<GOAL>μ (t ∩ s) = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>hs : MeasurableSet s<GOAL>(μ.restrict s) t = 0 ↔ μ (t ∩ s) = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<GOAL>μ.restrict s = 0 ↔ μ s = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>h : μ s = 0<GOAL>μ.restrict s = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.restrict ∅ = 0
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<GOAL>μ.restrict Set.univ = μ
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasurableSet t<GOAL>μ.restrict (s ∩ t) + μ.restrict (s \ t) = μ.restrict s
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>t : Set α<VAR>s : Set α<VAR>ht : MeasurableSet t<GOAL>μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s : Set α<VAR>hs : MeasurableSet s<VAR>t : Set α<GOAL>μ.restrict (s ∪ t) + μ.restrict (s ∩ t) = μ.restrict s + μ.restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : MeasureTheory.AEDisjoint μ s t<VAR>ht : MeasureTheory.NullMeasurableSet t μ<GOAL>μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t
<VAR>α : Type u_2<VAR>m0 : MeasurableSpace α<VAR>μ : MeasureTheory.Measure α<VAR>s t : Set α<VAR>h : Disjoint s t<VAR>ht : MeasurableSet t<GOAL>μ.restrict (s ∪ t) = μ.restrict s + μ.restrict t