mass — Mathlib

English

If μ_s i converges to μ in nhds, then their masses converge: (μ_s i).mass → μ.mass along the same filter.

Русский

Если μ_s i сходится к μ в nhds, то их массы сходятся: (μ_s i).mass → μ.mass вдоль того же фильтра.

LaTeX

$$$ \text{Tendsto } (i \mapsto (μ_s i).mass) F (\mathsf{nhds} (μ.mass)). $$$

Lean4

/-- Convergence of finite measures implies the convergence of their total masses. -/
theorem _root_.Filter.Tendsto.mass {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω}
    (h : Tendsto μs F (𝓝 μ)) : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass) :=
  (continuous_mass.tendsto μ).comp h

Похожие утверждения