measurePreserving_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem _root_.MeasureTheory.measurePreserving_fst [IsProbabilityMeasure ν] : MeasurePreserving Prod.fst (μ.prod ν) μ :=
  ⟨measurable_fst, by rw [map_fst_prod, measure_univ, one_smul]⟩

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