cond_univ

Mathlib.Probability.ConditionalProbability

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.cond_univ

English

If μ(s)=0 then μ[|s]=0.

Русский

Если μ(s)=0, то μ[|s]=0.

LaTeX

$$$h\\mu s = 0 \\Rightarrow μ[|s] = 0$$$

Lean4

@[simp]
theorem cond_univ [IsProbabilityMeasure μ] : μ[|Set.univ] = μ := by simp [cond, measure_univ, Measure.restrict_univ]

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

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

Разделы

Аффилиация

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