tendsto_zero_of_tendsto_zero_mass

English

There is an embedding of FiniteMeasure Ω into WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) via μ ↦ μ.toWeakDualBCNN.

Русский

Существует вложение FiniteMeasure Ω в WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) по μ ↦ μ.toWeakDualBCNN.

LaTeX

$$$ \text{IsEmbedding} (toWeakDualBCNN : \text{FiniteMeasure } \Omega \to WeakDual \mathbb{R}_{\ge 0} (\Omega \to^{} \mathbb{R}_{\ge 0})) . $$$

Lean4

/-- If the total masses of finite measures tend to zero, then the measures tend to zero. -/
theorem tendsto_zero_of_tendsto_zero_mass {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω}
    (mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 0)) : Tendsto μs F (𝓝 0) :=
  by
  rw [tendsto_iff_forall_testAgainstNN_tendsto]
  intro f
  convert tendsto_zero_testAgainstNN_of_tendsto_zero_mass mass_lim f
  rw [zero_testAgainstNN_apply]

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