prod_prod

Mathlib.MeasureTheory.Measure.FiniteMeasureProd

URI: https://scilib.ai/kg/mathlib#MeasureTheory.ProbabilityMeasure.prod_prod

English

The product of any probability measure with the zero measure is the zero measure: μ.prod 0 = 0.

Русский

Произведение любой вероятностной меры с нулевой мерой даёт нуль: μ.prod 0 = 0.

LaTeX

$$$\mu \mathrm{prod} 0 = 0$$$

Lean4

@[simp]
theorem prod_prod (s : Set α) (t : Set β) : μ.prod ν (s ×ˢ t) = μ s * ν t := by simp [coeFn_def]

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

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

Разделы

Аффилиация

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