measureReal_univ_eq_one

Mathlib.MeasureTheory.Measure.Real

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

English

If μ is a probability measure, then μ.real of the universal set is equal to 1.

Русский

Если μ — вероятностная мера, то μ.real(полное множество) = 1.

LaTeX

$$μ.real Set.univ = 1$$

Lean4

@[simp]
theorem measureReal_univ_eq_one [IsProbabilityMeasure μ] : μ.real Set.univ = 1 := by simp [Measure.real]

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

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

Разделы

Аффилиация

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