compProd_zero_right

Mathlib.Probability.Kernel.Composition.MeasureCompProd

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.compProd_zero_right

English

Composing any measure with the zero kernel yields the zero measure.

Русский

Сведение любой меры к нулевому ядру дает нулевую меру.

LaTeX

$$$μ ⊗_m (0 : \\text{Kernel } α β) = 0$$$

Lean4

@[simp]
theorem compProd_zero_right (μ : Measure α) : μ ⊗ₘ (0 : Kernel α β) = 0 := by simp [compProd]

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

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

Разделы

Аффилиация

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