instIsFiniteMeasureForallValNatMemFinsetInducedFamilyOfForallIic

English

Let μ = (μ_n) be a family of measures on the product spaces Π_{i ∈ Iic n} X_i for each n. If every μ_n is a finite measure, then for every finite index set I, the induced family ind uced by I, denoted indcedFamily μ I, is a finite measure.

Русский

Пусть μ = (μ_n) — семейство мер на произведениях Π_{i ∈ Iic n} X_i для каждого n. Если каждая μ_n является конечной мерой, то для любого конечного множества индексов I индуцированное семейство indcedFamily μ I также является конечной мерой.

LaTeX

$$$\\left(\\forall n,\\ IsFiniteMeasure (\\mu n)\\right) \\Rightarrow \\forall I:\\ Finset\\ \\mathbb{N},\\ IsFiniteMeasure (inducedFamily\\ \\mu\\ I)$$$

Lean4

instance [∀ n, IsFiniteMeasure (μ n)] (I : Finset ℕ) : IsFiniteMeasure (inducedFamily μ I) := by rw [inducedFamily];
  infer_instance

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