diracProba_toMeasure_apply — Mathlib

English

If id does not tend to x along a filter, then diracProba does not tend to diracProba x.

Русский

Если id не сходится к x вдоль фильтра, то diracProba не сходится к diracProba x.

LaTeX

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

Lean4

@[simp]
theorem diracProba_toMeasure_apply [MeasurableSingletonClass X] (x : X) (A : Set X) :
    (diracProba x).toMeasure A = A.indicator 1 x :=
  Measure.dirac_apply _ _

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