instIsProbabilityMeasureProdVolume

English

If both μ and ν are probability measures, then μ × ν is a probability measure.

Русский

Если μ и ν – вероятностные меры, то μ × ν является вероятностной мерой.

LaTeX

$$$\text{IsProbabilityMeasure}(μ × ν)$$$

Lean4

instance {α β : Type*} [MeasureSpace α] [MeasureSpace β] [IsProbabilityMeasure (volume : Measure α)]
    [IsProbabilityMeasure (volume : Measure β)] : IsProbabilityMeasure (volume : Measure (α × β)) :=
  prod.instIsProbabilityMeasure _ _

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