tendsto_diracProba_iff_tendsto — Mathlib

English

For any filter L and point x, Tendsto diracProba L toward diracProba x holds exactly when Tendsto id L toward x.

Русский

Для любого фильтра L и точки x выполняется, что сходится diracProba L к diracProba x тогда и только тогда, когда сходится id L к x.

LaTeX

$$$\\mathrm{Tendsto}\\, (\\mathrm{diracProba})\\, L\\,(\\mathcal{N}(\\mathrm{diracProba} x)) \\iff \\mathrm{Tendsto}\\ id\\, L\\,(\\mathcal{N} x)$$$

Lean4

theorem tendsto_diracProba_iff_tendsto [CompletelyRegularSpace X] {x : X} (L : Filter X) :
    Tendsto diracProba L (𝓝 (diracProba x)) ↔ Tendsto id L (𝓝 x) :=
  by
  constructor
  · contrapose
    exact not_tendsto_diracProba_of_not_tendsto L
  · intro h
    have aux := (@continuous_diracProba X _ _ _).continuousAt (x := x)
    simp only [ContinuousAt] at aux
    exact aux.comp h

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