instIsProbabilityMeasureForallInfinitePiNat

English

The measure infinitePiNat μ is a probability measure when μ is a family of probability measures.

Русский

Мера infinitePiNat μ является вероятностной мерой, если μ — семейство вероятностных мер.

LaTeX

$$$\text{instIsProbabilityMeasureForallInfinitePiNat } : \text{IsProbabilityMeasure } (\text{Measure.infinitePiNat } μ)$$$

Lean4

instance : IsProbabilityMeasure (Measure.infinitePiNat μ) := by rw [Measure.infinitePiNat]; infer_instance

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