Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ Tendsto (toFiniteMeasure ∘ μs) F (𝓝 (toFiniteMeasure μ)) ↔
    ∀ (f : Ω →ᵇ ℝ), 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 : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), ↑f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), ↑f ω ∂↑μ))
rw [tendsto_nhds_iff_toFiniteMeasure_tendsto_nhds]
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ),
      Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑((toFiniteMeasure ∘ μs) i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑(toFiniteMeasure μ)))) ↔
    ∀ (f : Ω →ᵇ ℝ), 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 (toFiniteMeasure ∘ μs) F (𝓝 (toFiniteMeasure μ)) ↔
    ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), ↑f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), ↑f ω ∂↑μ))
rw [FiniteMeasure.tendsto_iff_forall_integral_tendsto]
no goals
Ω : Type u_2
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → ProbabilityMeasure Ω
μ : ProbabilityMeasure Ω
⊢ (∀ (f : Ω →ᵇ ℝ),
      Tendsto (fun i => ∫ (x : Ω), ↑f x ∂↑((toFiniteMeasure ∘ μs) i)) F (𝓝 (∫ (x : Ω), ↑f x ∂↑(toFiniteMeasure μ)))) ↔
    ∀ (f : Ω →ᵇ ℝ), Tendsto (fun i => ∫ (ω : Ω), ↑f ω ∂↑(μs i)) F (𝓝 (∫ (ω : Ω), ↑f ω ∂↑μ))
rfl