volume_measurePreserving_piCongrLeft

English

Volume is preserved by piCongrLeft under index permutation for volume measures.

Русский

Объем сохраняется при перестановке индексов через piCongrLeft для мер объема.

LaTeX

$$volume_preserving_piCongrLeft(α,f)$$

Lean4

theorem volume_measurePreserving_piCongrLeft (α : ι → Type*) (f : ι' ≃ ι) [∀ i, MeasureSpace (α i)]
    [∀ i, SigmaFinite (volume : Measure (α i))] : MeasurePreserving (MeasurableEquiv.piCongrLeft α f) volume volume :=
  measurePreserving_piCongrLeft (fun _ ↦ volume) f

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