volume_preserving_piEquivPiSubtypeProd

English

The volume measure is preserved by the pi-equivalence between pi-space and the corresponding restricted product space.

Русский

Объемная мера сохраняется при переходе между пи-пространством и соответствующим ограниченным произведением.

LaTeX

$$volume_preserving_piEquivPiSubtypeProd(α,p)$$

Lean4

theorem volume_preserving_piEquivPiSubtypeProd (α : ι → Type*) [∀ i, MeasureSpace (α i)]
    [∀ i, SigmaFinite (volume : Measure (α i))] (p : ι → Prop) [DecidablePred p] :
    MeasurePreserving (MeasurableEquiv.piEquivPiSubtypeProd α p) :=
  measurePreserving_piEquivPiSubtypeProd (fun _ => volume) p

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