map_fst_prod — Mathlib

English

The pushforward of the product measure by the first projection equals the scalar ν(univ) times μ: Measure.map fst (μ × ν) = (ν univ) · μ.

Русский

Образы по первому проекции: импульс произведённой меры равен ν(univ) умноженному на μ.

LaTeX

$$$\mathrm{Measure.map} \mathrm{Prod.fst} (\mu \mathrm{.prod} ν) = (ν\, univ) \; \cdot \; μ$$$

Lean4

@[simp]
theorem map_fst_prod : Measure.map Prod.fst (μ.prod ν) = (ν univ) • μ :=
  by
  ext s hs
  simp [Measure.map_apply measurable_fst hs, ← prod_univ, mul_comm]

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