volume_preserving_pi_empty — Mathlib

English

If ι is empty, the pi_empty volume-preserving correspondence holds between the product measure and the dirac measure on Unit.

Русский

Если ι пуст, то сохраняющая меру соответствие между произведением и единичной мерой сохраняется.

LaTeX

$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.ofUniqueOfUnique}(\forall i, \alpha i)\; Unit\bigr)\; (\mathrm{volume})\; (\mathrm{volume}) $$$

Lean4

theorem volume_preserving_pi_empty {ι : Type u} (α : ι → Type v) [Fintype ι] [IsEmpty ι] [∀ i, MeasureSpace (α i)] :
    MeasurePreserving (MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit) volume volume :=
  measurePreserving_pi_empty fun _ => volume

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