English
The volume is preserved by the measurable equivalence arrowCongr' when transporting volumes across isomorphic base spaces.
Русский
Объём сохраняется при измеримом отображении arrowCongr', переводящем объёмы между исходными пространствами.
LaTeX
$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.arrowCongr'}(hα,hβ)\bigr)\; \mathrm{volume}\; \mathrm{volume} $$$
Lean4
/-- The measurable equiv `(α₁ → β₁) ≃ᵐ (α₂ → β₂)` induced by `α₁ ≃ α₂` and `β₁ ≃ᵐ β₂` is
volume preserving. -/
theorem volume_preserving_arrowCongr' {α₁ β₁ α₂ β₂ : Type*} [Fintype α₁] [Fintype α₂] [MeasureSpace β₁]
[MeasureSpace β₂] [SigmaFinite (volume : Measure β₂)] (hα : α₁ ≃ α₂) (hβ : β₁ ≃ᵐ β₂) (hm : MeasurePreserving hβ) :
MeasurePreserving (MeasurableEquiv.arrowCongr' hα hβ) :=
measurePreserving_arrowCongr' (fun _ ↦ volume) (fun _ ↦ volume) hα hβ (fun _ ↦ hm)
