tendsto_iff_weakDual_tendsto — Mathlib

English

Tendsto μs F (nhds μ) is equivalent to Tendsto μs.toWeakDualBCNN F (nhds μ.toWeakDualBCNN).

Русский

Сходимость μ_s в nhds μ эквивалентна сходящемуся образу в слабом двойственном пространстве.

LaTeX

$$$ \text{Tendsto } μ_s F (\mathsf{nhds} μ) \iff \text{Tendsto } (\lambda i. μ_s i.toWeakDualBCNN) F (\mathsf{nhds} (μ.toWeakDualBCNN)). $$$

Lean4

theorem tendsto_iff_weakDual_tendsto {γ : Type*} {F : Filter γ} {μs : γ → FiniteMeasure Ω} {μ : FiniteMeasure Ω} :
    Tendsto μs F (𝓝 μ) ↔ Tendsto (fun i ↦ (μs i).toWeakDualBCNN) F (𝓝 μ.toWeakDualBCNN) :=
  IsInducing.tendsto_nhds_iff ⟨rfl⟩

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