fst_prod — Mathlib

English

If ν is a probability measure, then the first marginal of the product μ × ν equals μ.

Русский

Если ν — вероятностьная мера, то первая маргинальная мера от μ × ν равна μ.

LaTeX

$$$$ (\\mu \\times \\nu).\\mathrm{fst} = \\mu \\quad [\\text{when } \\nu \\text{ is probability}] $$$$

Lean4

@[simp]
theorem fst_prod [IsProbabilityMeasure ν] : (μ.prod ν).fst = μ :=
  by
  ext1 s hs
  rw [fst_apply hs, ← prod_univ, prod_prod, measure_univ, mul_one]

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