instIsProbabilityMeasureForallVolume

English

If every i-space has a probability volume, then the product volume is a probability measure.

Русский

Если каждый объём μ_i на α_i является вероятностной мерой, то произведение объёмов на ∏ α_i является вероятностной мерой.

LaTeX

$$$\operatorname{IsProbabilityMeasure}(\mathrm{volume})$$$

Lean4

instance {α : ι → Type*} [∀ i, MeasureSpace (α i)] [∀ i, IsProbabilityMeasure (volume : Measure (α i))] :
    IsProbabilityMeasure (volume : Measure (∀ i, α i)) :=
  pi.instIsProbabilityMeasure _

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