volume_preserving_toLp — Mathlib

English

The measurable equivalence used in PiLp preserves the volume measure.

Русский

Измеримое эквивалентное отображение в PiLp сохраняет меру объема.

LaTeX

$$$\\text{PiLp.volumePreserving}$$$

Lean4

/-- The reverse direction of `PiLp.volume_preserving_measurableEquiv`, since
`MeasurePreserving.symm` only works for `MeasurableEquiv`s. -/
theorem volume_preserving_toLp : MeasurePreserving (@WithLp.toLp 2 (ι → ℝ)) :=
  (EuclideanSpace.volume_preserving_measurableEquiv ι).symm

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