Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 (toFiniteMeasure μ)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
rw [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds]
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 (toFiniteMeasure μ)) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (ω : Ω), ↑(↑f ω) ∂↑(μs i)) F (𝓝 (∫⁻ (ω : Ω), ↑(↑f ω) ∂↑μ))
exact FiniteMeasure.tendsto_iff_forall_lintegral_tendsto