volume_preserving_piFinsetUnion — Mathlib

English

Same as above, but for volumes: the volume measure is preserved by piFinsetUnion over disjoint Finsets.

Русский

Аналогично, но для объёма: снижение объёма сохраняется через piFinsetUnion для непересекающихся конечных множеств.

LaTeX

$$$ \mathrm{volume}\,\mathrm{Preserving}\bigl(\mathrm{MeasurableEquiv.piFinsetUnion}(\alpha,h)\bigr) $$$

Lean4

theorem volume_preserving_piFinsetUnion {ι : Type*} [DecidableEq ι] (α : ι → Type*) {s t : Finset ι} (h : Disjoint s t)
    [∀ i, MeasureSpace (α i)] [∀ i, SigmaFinite (volume : Measure (α i))] :
    MeasurePreserving (MeasurableEquiv.piFinsetUnion α h) volume volume :=
  measurePreserving_piFinsetUnion h (fun _ ↦ volume)

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