isProbabilityMeasure_iff

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

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

English

IsProbabilityMeasure μ iff μ univ = 1.

Русский

Мера μ является вероятностной тогда и только тогда, когда μ(всё множество) = 1.

LaTeX

$$IsProbabilityMeasure(μ) ↔ μ univ = 1$$

Lean4

theorem isProbabilityMeasure_iff : IsProbabilityMeasure μ ↔ μ univ = 1 :=
  ⟨fun _ ↦ measure_univ, IsProbabilityMeasure.mk⟩

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

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

Разделы

Аффилиация

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