volumePreserving_toMixed — Mathlib

English

The linear isomorphism toMixed between the Euclidean mixed space and the mixed space preserves volume.

Русский

Линейное изоморфное отображение toMixed между евклидовым смешанным пространством и смешанным пространством сохраняет объём.

LaTeX

$$volumePreserving (toMixed K)$$

Lean4

theorem volumePreserving_toMixed : MeasurePreserving (toMixed K)
    where
  measurable := (toMixed K).continuous.measurable
  map_eq := by
    rw [← (OrthonormalBasis.addHaar_eq_volume (euclidean.stdOrthonormalBasis K)), Basis.map_addHaar,
      stdOrthonormalBasis_map_eq, Basis.addHaar_eq_iff, Basis.coe_parallelepiped, ←
      measure_congr (ZSpan.fundamentalDomain_ae_parallelepiped (stdBasis K) volume),
      volume_fundamentalDomain_stdBasis K]

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