Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝ : IsCountablyGenerated L
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, ↑(fs i) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (↑f ω))
⊢ Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑(fs i) ω) ∂↑μ) L (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝ : IsCountablyGenerated L
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, ↑(fs i) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (↑f ω))
⊢ Tendsto (fun i => testAgainstNN μ (fs i)) L (𝓝 (testAgainstNN μ f))
apply
  (ENNReal.tendsto_toNNReal
      (lintegral_lt_top_of_boundedContinuous_to_nnreal (μ : Measure Ω) f).ne).comp
no goals
Ω : Type u_2
inst✝³ : MeasurableSpace Ω
inst✝² : TopologicalSpace Ω
inst✝¹ : OpensMeasurableSpace Ω
ι : Type u_1
L : Filter ι
inst✝ : IsCountablyGenerated L
μ : FiniteMeasure Ω
fs : ι → Ω →ᵇ ℝ≥0
c : ℝ≥0
fs_le_const : ∀ᶠ (i : ι) in L, ∀ᵐ (ω : Ω) ∂↑μ, ↑(fs i) ω ≤ c
f : Ω →ᵇ ℝ≥0
fs_lim : ∀ᵐ (ω : Ω) ∂↑μ, Tendsto (fun i => ↑(fs i) ω) L (𝓝 (↑f ω))
⊢ Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑(fs i) ω) ∂↑μ) L (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
exact tendsto_lintegral_nn_filter_of_le_const μ fs_le_const fs_lim