isProbabilityMeasure

Mathlib.MeasureTheory.Measure.Dirac

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.dirac.isProbabilityMeasure

English

The Dirac measure is sigma-finite.

Русский

Мера Дирака сигма-конечна.

LaTeX

$$$ SigmaFinite (dirac a) $$$

Lean4

instance isProbabilityMeasure {x : α} : IsProbabilityMeasure (dirac x) :=
  ⟨dirac_apply_of_mem <| mem_univ x⟩

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

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

Разделы

Аффилиация

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