volume_preserving_piFinSuccAbove — Mathlib

English

The volume measure is preserved by the piFinSuccAbove equivalence on the finite successor indexing.

Русский

Объем сохраняется под эквивалентностью piFinSuccAbove на конечном наборе индексов.

LaTeX

$$volume_preserving_piFinSuccAbove (α) (i) :$$

Lean4

theorem volume_preserving_piFinSuccAbove {n : ℕ} (α : Fin (n + 1) → Type u) [∀ i, MeasureSpace (α i)]
    [∀ i, SigmaFinite (volume : Measure (α i))] (i : Fin (n + 1)) :
    MeasurePreserving (MeasurableEquiv.piFinSuccAbove α i) :=
  measurePreserving_piFinSuccAbove (fun _ => volume) i

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