measurePreserving_finTwoArrow — Mathlib

English

There exists a canonical measurable equivalence FinTwoArrow between a product of two copies of a space and their product, preserving the product measure structure.

Русский

Существует каноническое измеримое эквивалентное отображение FinTwoArrow между произведением двух копий пространства и их произведением, сохраняющее меру.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.finTwoArrow}(\alpha)\bigr)\; (\mathrm{Measure.pi}\; (λ i. μ))\; (μ.prod μ) $$$

Lean4

theorem measurePreserving_finTwoArrow {α : Type u} {m : MeasurableSpace α} (μ : Measure α) [SigmaFinite μ] :
    MeasurePreserving MeasurableEquiv.finTwoArrow (Measure.pi fun _ => μ) (μ.prod μ) := by
  simpa only [Matrix.vec_single_eq_const, Matrix.vecCons_const] using measurePreserving_finTwoArrow_vec μ μ

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