volume_preserving_pi — Mathlib

English

The volume measure is preserved by the measurable arrowCongr' between product spaces induced by α ≃ α' and β ≃ᵐ β'.

Русский

Объём сохраняется при измеримом arrowCongr' между пространствами произведения, индуцированными α ≃ α' и β ≃ᵐ β'.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.arrowCongr'}(eα,eβ)\bigr)\; \mathrm{volume}\; \mathrm{volume} $$$

Lean4

theorem volume_preserving_pi {α' β' : ι → Type*} [∀ i, MeasureSpace (α' i)] [∀ i, MeasureSpace (β' i)]
    [∀ i, SigmaFinite (volume : Measure (β' i))] {f : (i : ι) → (α' i) → (β' i)} (hf : ∀ i, MeasurePreserving (f i)) :
    MeasurePreserving (fun (a : (i : ι) → α' i) (i : ι) ↦ (f i) (a i)) :=
  measurePreserving_pi _ _ hf

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