diracProba_toMeasure_apply'

Mathlib.MeasureTheory.Measure.DiracProba

URI: https://scilib.ai/kg/mathlib#MeasureTheory.diracProba_toMeasure_apply'

← MathLib Explorer

English

If μ equals diracProba x, then diracProbaInverse μ equals x.

Русский

Если μ = diracProba x, то diracProbaInverse μ = x.

LaTeX

$$$\\mu = \\mathrm{diracProba} x \\;\Rightarrow\\; \\mathrm{diracProbaInverse}\\mu = x$$$

Lean4

@[simp]
theorem diracProba_toMeasure_apply' (x : X) {A : Set X} (A_mble : MeasurableSet A) :
    (diracProba x).toMeasure A = A.indicator 1 x :=
  Measure.dirac_apply' x A_mble

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru