cond_empty

Mathlib.Probability.ConditionalProbability

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

English

Conditioning on the empty set yields the zero measure on the restricted space.

Русский

Условие по пустому множеству даёт нулевую меру на ограниченном пространстве.

LaTeX

$$$μ[|\\emptyset] = 0$$$

Lean4

@[simp]
theorem cond_empty : μ[|∅] = 0 := by simp [cond]

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

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

Разделы

Аффилиация

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