instNonemptySubtypeMeasureIsProbabilityMeasure

Mathlib.MeasureTheory.Measure.Dirac

URI: https://scilib.ai/kg/mathlib#MeasureTheory.instNonemptySubtypeMeasureIsProbabilityMeasure

English

There is a finite measure instance: dirac a is finite.

Русский

Существует конкретная конечная мера: dirac a - конечна.

LaTeX

$$$ IsFiniteMeasure (dirac a) $$$

Lean4

instance [hα : Nonempty α] : Nonempty { μ : Measure α // IsProbabilityMeasure μ } :=
  ⟨Measure.dirac hα.some, inferInstance⟩

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

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

Разделы

Аффилиация

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