infinitePiNat_map_restrict — Mathlib

English

Restricting the infinite product measure to a finite index set I yields the usual finite product measure: map I.restrict (infinitePi μ) = π i μ_i over i ∈ I.

Русский

Ограничение бесконечного произведения меры до конечного индекса I даёт обычное конечное произведение: map I.restrict (infinitePi μ) = π_i μ_i по i ∈ I.

LaTeX

$$$$ (\mathrm{infinitePi}\,\mu)\,\mathrm{map}\;I\!\restriction = \mathrm{Measure.pi}\;\bigl(\lambda i : I \mapsto \mu i\bigr). $$$$

Lean4

/-- Restricting the product measure to a product indexed by a finset yields the usual
product measure. -/
theorem infinitePiNat_map_restrict (I : Finset ℕ) : (infinitePiNat μ).map I.restrict = Measure.pi fun i : I ↦ μ i :=
  isProjectiveLimit_infinitePiNat μ I

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