measureReal_le_one

Mathlib.MeasureTheory.Measure.Typeclasses.Probability

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

← MathLib Explorer

English

IsProbabilityMeasure μ is equivalent to μ(univ) = 1.

Русский

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

LaTeX

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

Lean4

theorem measureReal_le_one {μ : Measure α} [IsZeroOrProbabilityMeasure μ] {s : Set α} : μ.real s ≤ 1 :=
  ENNReal.toReal_le_of_le_ofReal zero_le_one (ENNReal.ofReal_one.symm ▸ prob_le_one)

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

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

Разделы

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

Аффилиация

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