infinitePi_map_restrict — Mathlib

English

Repeated: Restricting infinitePi μ to I gives the finite product π over I.

Русский

Повторение: ограничение infinitePi μ до I даёт конечное произведение π по I.

LaTeX

$$$$ (\mathrm{infinitePi}\,\mu)\mapsto I\!\restriction = \mathrm{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 infinitePi_map_restrict {I : Finset ι} : (Measure.infinitePi μ).map I.restrict = Measure.pi fun i : I ↦ μ i :=
  isProjectiveLimit_infinitePi μ I

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