instIsFiniteMeasure

Mathlib.MeasureTheory.Measure.Dirac

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

English

The Dirac measure δ_a is sigma-finite for any a.

Русский

Мера Дирака δ_a сигма-конечна для любого a.

LaTeX

$$$ (dirac a) \\text{ is } \\ SigmaFinite $$$

Lean4

instance instIsFiniteMeasure {a : α} : IsFiniteMeasure (dirac a) :=
  inferInstance

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

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

Разделы

Аффилиация

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