instIsProbabilityMeasure — Mathlib

English

If both component measures are finite, then the volume on the product space is finite.

Русский

Если обе компоненты имеют конечный объём, то объём произведения конечен.

LaTeX

$$$\mathrm{volume}_{\alpha \times \beta} < \infty$ if $\mathrm{volume}_\alpha < \infty$ and $\mathrm{volume}_\beta < \infty$$$

Lean4

instance instIsProbabilityMeasure {α β : Type*} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (μ : Measure α)
    (ν : Measure β) [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] : IsProbabilityMeasure (μ.prod ν) :=
  ⟨by rw [← univ_prod_univ, prod_prod, measure_univ, measure_univ, mul_one]⟩

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