Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.130020
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (y : Ω →ᵇ ℝ≥0),
      Tendsto (fun i => ↑(↑(topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (toWeakDualBCNN (μs i))) y) F
        (𝓝 (↑(↑(topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (toWeakDualBCNN μ)) y))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ↑(toWeakDualBCNN (μs i)) f) F (𝓝 (↑(toWeakDualBCNN μ) f))
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.130020
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ Tendsto μs F (𝓝 μ) ↔ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ↑(toWeakDualBCNN (μs i)) f) F (𝓝 (↑(toWeakDualBCNN μ) f))
rw [tendsto_iff_weak_star_tendsto, tendsto_iff_forall_eval_tendsto_topDualPairing]
no goals
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.130020
inst✝⁵ : SMul R ℝ≥0
inst✝⁴ : SMul R ℝ≥0∞
inst✝³ : IsScalarTower R ℝ≥0 ℝ≥0∞
inst✝² : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_1
F : Filter γ
μs : γ → FiniteMeasure Ω
μ : FiniteMeasure Ω
⊢ (∀ (y : Ω →ᵇ ℝ≥0),
      Tendsto (fun i => ↑(↑(topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (toWeakDualBCNN (μs i))) y) F
        (𝓝 (↑(↑(topDualPairing ℝ≥0 (Ω →ᵇ ℝ≥0)) (toWeakDualBCNN μ)) y))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ↑(toWeakDualBCNN (μs i)) f) F (𝓝 (↑(toWeakDualBCNN μ) f))
rfl