snd_prod — Mathlib

English

Let μ be a probability measure on α and ν a measure on β. Then the second marginal of their product is ν.

Русский

Пусть μ – вероятность на α, ν – мера на β. Тогда вторая маргинальная мера произведения μ × ν равна ν.

LaTeX

$$$\\operatorname{snd}(\\mu \\times \\nu) = \\nu$$$

Lean4

@[simp]
theorem snd_prod [IsProbabilityMeasure μ] : (μ.prod ν).snd = ν :=
  by
  ext1 s hs
  rw [snd_apply hs, ← univ_prod, prod_prod, measure_univ, one_mul]

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