measurePreserving_snd — Mathlib

English

The product measure on a product of spaces with open-positive volume is again open-positive.

Русский

Произведение мер сохраняет свойство открытой положительности по объёму на произведении пространств.

LaTeX

$$$\text{IsOpenPosMeasure}(\mathrm{volume}_{X \times Y})$$$

Lean4

theorem _root_.MeasureTheory.measurePreserving_snd [IsProbabilityMeasure μ] : MeasurePreserving Prod.snd (μ.prod ν) ν :=
  ⟨measurable_snd, by rw [map_snd_prod, measure_univ, one_smul]⟩

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