snd_dirac_unit_compProd_const — Mathlib

English

Let μ be a measure on β. The second marginal of the product of the Dirac measure on the unit type with the constant kernel μ is μ.

Русский

Пусть μ — мера на β. Второй маргинал произведения дираковской меры на единичном множестве и константного ядра μ равен μ.

LaTeX

$$$\\operatorname{snd}\\Big(\\operatorname{dirac}(\\mathrm{Unit}) \\otimes_{\\mathrm{m}} \\mathrm{Kernel.const}(\\mathrm{Unit}, \\mu)\\Big) = \\mu$$$

Lean4

theorem snd_dirac_unit_compProd_const (μ : Measure β) [SFinite μ] : snd (Measure.dirac () ⊗ₘ Kernel.const Unit μ) = μ :=
  by simp

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