volume_negAt_plusPart — Mathlib

English

If A is measurable, then the volume of negAt s '' (plusPart A) equals the volume of plusPart A; vol(negAt s '' (plusPart A)) = vol(plusPart A).

Русский

Если A измеримо, то объем negAt s '' plusPart A равен объему плюсPart A.

LaTeX

$$volume(negAt(s)''(plusPart(A))) = volume(plusPart(A))$$

Lean4

/-- The image of the `plusPart` of `A` by `negAt` have all the same volume as `plusPart A`. -/
theorem volume_negAt_plusPart (hm : MeasurableSet A) : volume (negAt s '' (plusPart A)) = volume (plusPart A) := by
  rw [← negAt_symm, ContinuousLinearEquiv.image_symm_eq_preimage,
    volume_preserving_negAt.measure_preimage (measurableSet_plusPart hm).nullMeasurableSet]

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