volume_measurePreserving_arrowProdEquivProdArrow

English

If each coordinate space has a volume invariant under inversion, then the product space's volume is invariant under inversion.

Русский

Если каждая координатная часть имеет объем, инвариантный относительно обращения, то объём произведения инвариантен относительно обращения.

LaTeX

$$$\forall i, IsInvInvariant(volume_i) \Rightarrow IsInvInvariant(volume)$$$

Lean4

theorem volume_measurePreserving_arrowProdEquivProdArrow (α β γ : Type*) [MeasureSpace α] [MeasureSpace β] [Fintype γ]
    [SigmaFinite (volume : Measure α)] [SigmaFinite (volume : Measure β)] :
    MeasurePreserving (MeasurableEquiv.arrowProdEquivProdArrow α β γ) :=
  measurePreserving_arrowProdEquivProdArrow α β γ (fun _ ↦ volume) (fun _ ↦ volume)

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