English
Let μ = (μ_n) be a family where each μ_n is a probability measure. Then for every finite I, the induced family ind uced by I is a probability measure: IsProbabilityMeasure (inducedFamily μ I).
Русский
Пусть μ = (μ_n) — семейство, где каждая μ_n является вероятностной мерой. Тогда для любого конечного I индуцированное семейство μ I является вероятностной мерой: IsProbabilityMeasure (inducedFamily μ I).
LaTeX
$$$\\left(\\forall n,\\ IsProbabilityMeasure (\\mu n)\\right) \\Rightarrow \\forall I:\\ Finset\\ \\mathbb{N},\\ IsProbabilityMeasure (inducedFamily\\ \\mu\\ I)$$$
Lean4
instance [∀ n, IsProbabilityMeasure (μ n)] (I : Finset ℕ) : IsProbabilityMeasure (inducedFamily μ I) :=
by
rw [inducedFamily]
exact Measure.isProbabilityMeasure_map (measurable_restrict₂ _).aemeasurable
