α : Type u_2
E : Type u_3
F : Type ?u.973542
𝕜 : Type ?u.973545
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
f : α → E
hf : HasFiniteIntegral f
l : Filter ι
s : ι → Set α
hs : Tendsto (↑↑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun e => ‖∫ (x : α) in s e, f x ∂μ‖) l (𝓝 0)
α : Type u_2
E : Type u_3
F : Type ?u.973542
𝕜 : Type ?u.973545
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
f : α → E
hf : HasFiniteIntegral f
l : Filter ι
s : ι → Set α
hs : Tendsto (↑↑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun i => ∫ (x : α) in s i, f x ∂μ) l (𝓝 0)
rw [tendsto_zero_iff_norm_tendsto_zero]
α : Type u_2
E : Type u_3
F : Type ?u.973542
𝕜 : Type ?u.973545
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
f : α → E
hf : HasFiniteIntegral f
l : Filter ι
s : ι → Set α
hs : Tendsto (↑↑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun a => ↑‖∫ (x : α) in s a, f x ∂μ‖₊) l (𝓝 0)
α : Type u_2
E : Type u_3
F : Type ?u.973542
𝕜 : Type ?u.973545
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
f : α → E
hf : HasFiniteIntegral f
l : Filter ι
s : ι → Set α
hs : Tendsto (↑↑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun e => ‖∫ (x : α) in s e, f x ∂μ‖) l (𝓝 0)
simp_rw [← coe_nnnorm, ← NNReal.coe_zero, NNReal.tendsto_coe, ← ENNReal.tendsto_coe,
  ENNReal.coe_zero]
no goals
α : Type u_2
E : Type u_3
F : Type ?u.973542
𝕜 : Type ?u.973545
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : CompleteSpace E
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : SMulCommClass ℝ 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
f✝ g : α → E
m : MeasurableSpace α
μ : Measure α
ι : Type u_1
f : α → E
hf : HasFiniteIntegral f
l : Filter ι
s : ι → Set α
hs : Tendsto (↑↑μ ∘ s) l (𝓝 0)
⊢ Tendsto (fun a => ↑‖∫ (x : α) in s a, f x ∂μ‖₊) l (𝓝 0)
exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
  (tendsto_set_lintegral_zero (ne_of_lt hf) hs) (fun i => zero_le _)
  fun i => ennnorm_integral_le_lintegral_ennnorm _