Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.153372
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 Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ↑(toWeakDualBCNN (μs i)) f) F (𝓝 (↑(toWeakDualBCNN μ) f))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.153372
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 => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
rw [tendsto_iff_forall_toWeakDualBCNN_tendsto]
no goals
Ω : Type u_2
inst✝⁶ : MeasurableSpace Ω
R : Type ?u.153372
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 Ω
⊢ (∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ↑(toWeakDualBCNN (μs i)) f) F (𝓝 (↑(toWeakDualBCNN μ) f))) ↔
    ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => ∫⁻ (x : Ω), ↑(↑f x) ∂↑(μs i)) F (𝓝 (∫⁻ (x : Ω), ↑(↑f x) ∂↑μ))
simp_rw [toWeakDualBCNN_apply _ _, ← testAgainstNN_coe_eq, ENNReal.tendsto_coe,
  ENNReal.toNNReal_coe]